Rewriting-based model checking methods

Model checking;Rewriting logic;Formal methods;Temporal logic;Infinite-state systems;Cyber-physical systems

Bae, Kyungmin

关键词: Model checking;    Rewriting logic;    Formal methods;    Temporal logic;    Infinite-state systems;    Cyber-physical systems;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/50553/Kyungmin_Bae.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

Model checking is an automatic technique for verifying concurrent systems. The properties of the system to be verified are typically expressed as temporal logic formulas, while the system itself is formally specified as a certain system specification language, such as computational logics and conventional programming languages. Rewriting logic is a highly expressive computational logic for effectively defining a formal executable semantics of a wide range of system specification languages. This dissertation presents new rewriting-based model checking methods and tools to effectively verify concurrent systems by means of their rewriting-based formal semantics.Specifically, this work develops: (i) efficient model checking algorithms and a tool for a suitable property specification language, namely, linear temporal logic of rewriting (LTLR) formulas under parameterized fairness; (ii) various infinite-state model checking techniques for LTLR properties, such as equational abstraction, folding abstraction, predicate abstraction, and narrowing-based symbolic model checking; and (iii) the Multirate PALS methodology for making it possible to model check virtually synchronous cyber-physical systems by reducing their system complexity.To demonstrate rewriting-based model checking, we have developed fully integrated modeling and model checking tools for two widely-used embedded system modeling languages, AADL and Ptolemy II. This approach provides a model-engineering process that combines the advantages of an existing modeling language with automatic rewriting-based model checking.