|
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
|