University of Konstanz
Graduiertenkolleg / PhD Program
Computer and Information Science

Graduation Talks


Incomplete property checking for asynchronous reactive systems


Wei Wei, University Konstanz
Konstanz, Germany

date & place

Wednesday, 31.01.2007, 15:15 h
Room C252


Asynchronous reactive systems find applications in a wide range of software systems such as communication protocols, embedded software systems, etc. Formal approaches to the verification of these systems, such as model checking, are often difficult because these systems usually possess extremely large or even infinite state spaces. We propose an integer programming solving based verification framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. In such way we avoid the exploration of the whole state space of the system. More precisely, we derive a necessary condition for the violation of the considered property from the control flow cycles in the system. We further encode the necessary condition into an integer linear programming problem (ILP) whose solution space represents the undesired behavior. The infeasibility of the ILP problem then establishes the satisfaction of the property by the system. While the precision of our framework remains an issue, we propose a counterexample-guided abstraction refinement technique based on the discovery of dependencies among control flow cycles. We have applied our framework to the verification of the buffer boundedness and livelock freedom properties, and developed several prototype tools with which we obtained promising experimental results on toy as well as real life system models.