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.
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:
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.
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.
You can find here a list of our published work.