实时的系统的多范式集成建模与验证
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms
摘要：
复杂系统通常有许多不同的部分和方面，具有不同的特征。在多范式建模方法中，具有不同性质的形式主义被组合使用来描述系统的互补部分和方面。这可以对建模活动产生有益的影响，因为不同的范例可以更好地适合于描述系统的不同方面。虽然每一种范式都对系统的许多方面提供了不同的看法，但至关重要的是，一个连贯的综合模型是从各种部分描述的组合中产生的。在本文中，我们提出了一种技术，同一系统的不同方面，不同的形式主义建模，同时保持各种模型紧密结合在一起。此外，我们的方法利用了一个有界可满足性检查器提供的灵活性编码的命题可满足性（SAT）问题的集成模型的验证问题，这使得用户可以进行形式化验证活动的整个模型和部分。通过一个监测系统的例子说明了该方法的有效性。
英文摘要：
Complex systems typically have many different parts and facets, with different characteristics. In a multi-paradigm approach to modeling, formalisms with different natures are used in combination to describe complementary parts and aspects of the system. This can have a beneficial impact on the modeling activity, as different paradigms an be better suited to describe different aspects of the system. While each paradigm provides a different view on the many facets of the system, it is of paramount importance that a coherent comprehensive model emerges from the combination of the various partial descriptions. In this paper we present a technique to model different aspects of the same system with different formalisms, while keeping the various models tightly integrated with one another. In addition, our approach leverages the flexibility provided by a bounded satisfiability checker to encode the verification problem of the integrated model in the propositional satisfiability (SAT) problem; this allows users to carry out formal verification activities both on the whole model and on parts thereof. The effectiveness of the approach is illustrated through the example of a monitoring system.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
