Verification methods and techniques for parametrized systems

Parameterization appears naturally in modeling and verifying protocols. A lot of work have been devoted in the project to the development of new methods, techniques, and tools for parametric reasoning.

1. The symbolic reachability analysis paradigm has been extended to parametrized systems. The decidability of the verification problem (of safety properties) has been established for significant classes of parametrized systems and automatic verification methods and tools have been developed for more general (undecidable) cases.
2. A framework, called Regular Model Checking, has been introduced for reasoning about networks of finite-state systems arranged in linear, ring-like, or tree-like topologies. In this framework, sets of configurations of arbitrary lengths are represented by means of regular languages (automata on words or trees), systems are modeled as regular relations (transductions). This framework has also been extended to systems generating some classes of nonregular languages.
3. New approaches for parametric reasoning have been introduced based on abstraction, and on systematic methods for generating and checking inductive invariants.
4. New tools have been developed for the analysis of extended automata with parametric guards. These tools have been applied to the verification of protocols with complex parametric timing constraints.