CMU-CS-04-145
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-04-145

An Expressive Verification Framework for State/Event Systems

Sagar Chaki, Edmund Clarke, Orna Grumberg*, Joël Ouaknine,
Natasha Sharygina, Tayssir Touili, and Helmut Veith**

May 2004

CMU-CS-04-145.ps
CMU-CS-04-145.pdf


Keywords: Temporal logic, compositional verification, software model checking


Specification languages for concurrent software systems need to combine practical algorithmic efficiency with high expressive power and the ability to reason about both states and events. We address this question by defining a new branching-time temporal logic SE-AO which integrates both state-based and action-based properties. SE-AO is universal, i.e., preserved by the simulation relation, and thus amenable to counterexample-guided abstraction refinement. We provide a model-checking algorithm for this logic, and describe a compositional abstraction-refinement loop which exploits the natural decomposition of the concurrent system; the abstraction and refinement steps are performed over each component separately, and only the model checking step requires an explicit composition of the abstracted components. For experimental evaluation, we have integrated the presented algorithms in the software verification tool MAGIC, and determined a previously unknown race condition error in a piece of an industrial robot control software.

17 pages

*The Technion, Haifa, Israel
**Technische Universitat Munchen, Munich, Germany


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu