Parametrized Systems

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.

Publications

You can find here a list of our published work.