Issue No. 02 - Feb. (2013 vol. 39)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2011.1
Stefan Leue , University of Konstanz, Konstanz
Wei Wei , SAP AG, Darmstadt
Asynchronous reactive systems form the basis of a wide range of software systems, for instance in the telecommunications domain. It is highly desirable to rigorously show that these systems are correctly designed. However, traditional formal approaches to the verification of these systems are often difficult because asynchronous reactive systems usually possess extremely large or even infinite state spaces. We propose an integer linear program (ILP) solving-based property checking framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. We apply our framework to the checking of the buffer boundedness and livelock freedom properties, both of which are undecidable for asynchronous reactive systems with an infinite state space. We illustrate the application of the proposed checking methods to Promela, the input language of the SPIN model checker. While the precision of our framework remains an issue, we propose a counterexample guided abstraction refinement procedure based on the discovery of dependences among control flow cycles. We have implemented prototype tools with which we obtained promising experimental results on real-life system models.
Unified modeling language, Complexity theory, Analytical models, Message passing, Integer linear programming, Mathematical model, Cost accounting, Promela, Software verification, formal methods, property checking, integer linear programming, static analysis, abstraction, refinement, counterexamples, asynchronous communication, buffer boundedness, livelock freedom, control flow cycles, cycle dependences, UML
S. Leue and W. Wei, "Integer Linear Programming-Based Property Checking for Asynchronous Reactive Systems," in IEEE Transactions on Software Engineering, vol. 39, no. , pp. 216-236, 2013.