Rewriting-based model checking methods

Bae, Kyungmin

Permalink

https://hdl.handle.net/2142/50553 Copy

Description

Title

Rewriting-based model checking methods

Author(s)

Bae, Kyungmin

Issue Date

2014-09-16

Director of Research (if dissertation) or Advisor (if thesis)

Meseguer, José

Doctoral Committee Chair(s)

Meseguer, José

Committee Member(s)

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

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

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

Abstract

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.

Graduation Semester

2014-08

Permalink

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

Copyright and License Information

Copyright 2014 Kyungmin Bae

Owning Collections