Verification with Integer and Constraint Programming

Introduction

Current Research

Cooperations, Financial Support

Publications

Links to Related Sites

Selected References

Current Members:


 

Introduction:

In the verification of distributed systems, one of the most interesting questions concerns the proof of special properties like reachability, deadlock-freeness and liveness. There exist different approaches for the treatment of such questions, e.g. exact methods and methods based on tests. Exact methods result in a "yes/no"-answer and therefore they can be used both for verification and falsification. Another possibility is testing a system for a special property. At this we will understand a test as a method that terminates always and confirms the desired property if it holds. Otherwise the test permits no statement on account of wrong-positive solutions. Methods based on tests are semi-decision methods because they produce only a "yes/don't know"- or "no/don't know"-answer.

A very important aspect in the verification of parallel systems is the development of techniques that do not suffer from the state space explosion problem. It arises from the fact that in a distributed systems the number of states can grow exponentially in the number of its components. Accordingly, every technique that enumerates explicitly all states of a system can not be applied to practical-sized systems.

From this point of view our motivation follows for the use of verification techniques based on constraint programming. The biggest advantage of these techniques is that they do not analyse the whole state space and from there avoid the state space explosion problem. Generally, a constraint can be interpreted as a restriction of the search space, and mathematically modelled as a relation about the variables of the search space. Caused by the restricted search space, systems with infinite state spaces can be verified with these methods now. For a classification of constraint programming methods there have to be considered both the nature of the constraints (linear, non-linear, convex, non-convex) and the nature of the search space (discrete, continuous, finite, infinite). The beginnings of constraint programming base on Jaffar and Lassez [JAF87]. In the past one has understood constraint programming rather as an embedding in logical programming whereas today it is more assigned to mathematical programming. Integer and constraint programming are supported by tools like 2lp [MCT96], which is an algebraical modelling language, CPLEX [CPL97], lp_solve, that are linear programming solvers, or OPBDP [BAR95] (Optimization Pseudo-Boolean Davis-Putnam).

 

Current Research:

In our current researches we use Petri nets [REI85] as base for modelling distributed systems. In the area of 1-safe Petri nets the interesting properties like reachability, deadlock-freeness and liveness are PSPACE-complete. Complexity analysis has shown that there do not exist both exact and efficient methods for the verification of these properties, generally. Structural concepts of Petri nets like place and transition invariants, traps and siphons are suitable mechanisms for the verification of parallel systems with constraint programming. The structures can be formalized algebraically, and therefore they can be used for tests implemented with linear equation systems. One of the most popular methods uses the marking equation which can be easily derived from the net description and its initial marking. The marking equation has been proven as a suitable linear algebraic criterion for reachability [DES96, DEE95, MUR89, MEL98]. It can be seen as a set of linear constraints that every reachable marking must satisfy. In task to verify a special property we add to the marking equation a set of new constraints which specify the markings which do not satisfy the desired property. Afterwards we try to find a solution for the restricted equation system with methods of integer programming. If there does not exist such a solution, then all reachable markings fulfill the desired property. So a constraint can be seen as a restriction to the set of reachable markings. Applying the marking equation to acyclic nets one obtains not only an essential but also sufficient criterion for reachability questions. At this point we obtain even an exact method, because each net can be unfolded into an acyclic net. However, problems arise with the verification of systems that communicate with shared variables. So some properties like the mutual exclusion of critical regions (there are some mutex algorithms well known in the literature) can not be verified only with the marking equation. But in this context the structural concept of traps has been proven successfully as completion to the marking equation. The combination of traps and marking equation represents a suitable technique for the successful verification of the mutual exclusion property for the algorithms. In [ME96] we show, that marking equation and trap equation both together significantly extend the range of verifiable systems.

Another interesting task is the verification of properties that are expressed as LTL-formulae (linear-time temporal logic). Vardi and Wolper introduced an automata theoretic approach to this problem [VAW86], but their approach suffers from the state-explosion problem. Several suggestions have been made to avoid this problem by means of different techniques like stubborn sets [VAL92] or sleep sets [GDE96]. In [EM97] we introduce another technique that bases on the automata theoretic approach to model checking, but avoids the state explosion problem. At this we construct a product Büchi net from a Petri net modelling the semantic behaviour of the associated concurrent system and a Büchi automaton accepting all sequences that do not satisfy the formula to be checked. Then we can reduce the model checking problem to a 'net-emptiness' problem of the product Büchi net. Using 2lp we have implemented a semi-decision test based on the notion of T-invariants and applied the test to a leader election and to a snapshot algorithm.


Cooperations:

Financial Support:


Publications:

[Postscript] [PDF]



Links to Related Sites:


Selected References:

[BAR95]
  P. Barth. A Davis-Putnam Based Enumeration Algorithm for Linear Pseudo-Boolean Optimization. Technischer Bericht MPI-I-95-2-003, Max-Planck-Institut für Informatik, Saarbrücken, 1995.
[CPL97]
  CPLEX Optimization Inc. Using the CPLEX 5.0 Callable Library and CPLEX Mixed Integer Library. ILOG, 1997.
[DEE95]
  J. Desel, J. Esparza. Free-choice Petri Nets. Cambridge Tracts in Theoretical Computer Science, vol. 40, Cambridge University Press, 1995.
[DES96]
  J. Desel. Petrinetze, Lineare Algebra und Lineare Programmierung. Habilitationsschrift, Humbolt-Universität zu Berlin, 1996.
[GDE96]
  P. Godefroid. Partial-Order Methods for Verification of Concurrent Systems. In Lecture Notes in Computer Science, vol. 1032, Springer, 1996.
[JAF87]
  J. Jaffar, J.-L. Lassez. Constraint logic programming. In 14th Annual ACM Symposium on Principles of Programming Languages, 1987.
[MCT96]
  K. McAloon, C. Tretkoff. Optimization and Computational Logic. John Wiley & Sons, 1996.
[MEL98]
  S. Melzer. Verifikation verteilter Systeme mit linearer- und Constraint- Programmierung. Dissertation, Technische Universität München, 1998.
[MUR89]
  T. Murata. Petri nets: Properties, Analysis and Applications. In Proceedings of the IEEE 77(4): 541 - 580, 1989.
[REI85]
  W. Reisig. Petri Nets. EATCS Monographs on Theoretical Computer Science, vol. 4, Springer-Verlag, 1985.
[VAL92]
  Antti Valmari. A Stubborn Attack on State Explosion. Formal Methods in System Design, 1: 297 - 322, 1992.
[VAW86]
  M. Vardi, P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logics in Computer Science, pages 322 - 331, Cambridge, June 1986.

vi powered! HTML4.0 checked!
Tue June 08 1999