In the domain of software verification, there is an evident need for specification formalisms and efficient algorithms to verify branching-time properties that involve both data and communication. We address this problem by defining a new branching-time temporal logic SE-AΩ which integrates both state-based and action-based properties. SE-AΩ 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 our algorithms within the ComFoRT reasoning framework and used them to verify a piece of industrial robot control software.
Proceedings of IFM 05, LNCS 3771, 2005. 17 pages.
PostScript /
PDF
© 2005
Springer-Verlag.