Department of Information Technology

Parametrized Systems

21137482.thm.jpg Parametrized systems arise when we verify systems consisting of an arbitrary number of components (sometimes) together with a global controller. Examples of such systems include mutual exclusion protocols, cache coherence protocols, broadcast protocols, etc. We perform a so called parameterized verification; that is, we verify the correctness of a property, mutual exclusion for example, regardless of the number of processes inside the system.

Contributions

We designed several constraint systems, that we sometimes combined with abstraction, and used them in the tools we are implementing.

Minimal Condition Constraints

At least two processes are in their critical sections is a typical example of such a constraint. The constraint specifies a minimal number of conditions to be satisfied by a configuration. Minimal condition constraints arise naturally when modelling parameterized systems. We have applied this framework to design verification algorithms for different classes of parameterized systems:

  • Unordered systems with an unbounded number of real-valued clocks: for example networks of timed processes and timed Petri nets.
  • Finite-state automata, operating on possibly unbounded data domains, ordered in an array, with local and global conditions as transitions' guard: communication via broadcast, rendez-vous and shared variables.
Regular Expressions

Minimal Condition Constraints can sometimes be seen as a special case of Regular Expressions. Regular Expressions, i.e automata, are used mainly in Regular Model Checking as the building blocs of a unifying framework for algorithmic verification of infinite-state systems with, e.g., queues, stacks, integers, or a parameterized topology. An important tool in Regular Model Checking is the ability to compute the transitive closure of a regular relation, i.e., the effect of arbitrarily long execution sequences. In the case of length preserving relations, we focus on two approaches: In the first one, Regular Model Checking the states are represented by strings over a finite alphabet; in the second one, Tree Regular Model Checking, is an extension of the first approach where states are represented by trees over a finite ranked alphabet and the transition relation by a bottom-up tree transducer.

View Abstraction

We developed a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees.

Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue.

We show that the method is complete for a large class of well quasi-ordered systems including Petri nets.
Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

Publications

You can find here a list of our published work.

Updated  2015-03-27 21:55:32 by Frédéric Haziza.