Introduction
Cooperations, Financial Support Current Members: |
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).
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.
[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. |