Rewriting-based model checking methods

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2014

Author dc:creator

• Bae, Kyungmin

Contributors dc:contributor

• Meseguer, José
• Agha, Gul A.
• Clarke, Edmund M.
• Roşu, Grigore

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

Statement dc:rights

• Copyright 2014 Kyungmin Bae

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/50553

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/50553