Homepage
en
ru

Checker of Asynchronous Parameterized Systems (CheAPS)

CheAPS is a (model) Checker of Asynchronous Parameterized Systems. The project was principally developed in the framework of my PhD thesis "Verification of Parameterized Models of Distributed Systems" and INTAS Project on Practical Formal Verification Using Automated Reasoning and Model Checking.

Brief Overview

Take a look at ten minute tutorial and the manual.

Goal

The goal of CheAPS project is to develop a practical tool to perform Parameterized Model Checking (PMC), i.e. to check the given specification `phi` on an infinite family `F` of finite-state models. In a special case, each model `M_n` of the family `F` is composed of `n` instances of process `P` and one static process `Q`, i.e. amath M_n = Q\ |\ |\ P\ |\ |\ ...\ | |\ P endamath. In general, models of the family `F` are generated by context-free network grammars like in [CGJ95].

Rationale

PMC problem was actively researched for several decades (see [KZ07] for a short review of the techniques in the area). The solution to PMC problem for the given family `F` in practice gives two important applications:

  • Design scalability is proved: specification is preserved while the number of communicating processes grows. While this property is often assumed by the authors of models it may be violated. Thus, it has to be proven.
  • The model checking of a model with a large number of isomorphic communicating processes may be reduced to the model checking of a smaller model comprised of a smaller number of processes. In view of state explosion problem this kind of reduction may play a crucial role in the success of model checking.

Scope

CheAPS can be applied to a parameterized family `F` of models with the following constraints:
  • Processes are considered as finite-state labelled transition systems. In CheAPS a (rather small) subset of Promela language is used to describe process prototypes.
  • There is a fixed number of prototype processes.
  • Instances of prototype processes are isomorphic. It means, for instance, that prototypes should not have transitions dependant on value of process id.
  • Each model of `F` is generated by a context-free network grammar `G` associated with the family `F`. In the grammar `G` process prototype is attached to each terminal, and grammar rules describe the rules of parallel composition.
  • Asynchronous (interleaving) parallel composition of processes is used.
  • Processes communicate by rendezvous message passing only (however, message channels may be modelled as processes).

Applications

CheAPS was applied to verify several small parameterized systems (like a wave algorithm and Milner's scheduler) as well as to verify a parameterized model of Resource reSerVation Protocol [KZ07, KZ09].

Distribution and License

CheAPS is distributed under BSD-like license except for 3rdparty/pangen4.h from Spin which is distributed under the license of its respected authors (I use DFA representation from it). The latest version can be downloaded at download page.

Back to main page