Files in this item



application/pdfKyungmin_Bae.pdf (4MB)
(no description provided)PDF


Title:Rewriting-based model checking methods
Author(s):Bae, Kyungmin
Director of Research:Meseguer, José
Doctoral Committee Chair(s):Meseguer, José
Doctoral Committee Member(s):Agha, Gul A.; Clarke, Edmund M.; Roşu, Grigore
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(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.
Issue Date:2014-09-16
Rights Information:Copyright 2014 Kyungmin Bae
Date Available in IDEALS:2014-09-16
Date Deposited:2014-08

This item appears in the following Collection(s)

Item Statistics