• What is the Model-Checking Kit?
• The Kit in a nutshell
• Why a Kit?
• Intended users
• The Kit's strengths
• The Kit's weaknesses
• Which description languages can I use?
• Which checkers can I use?
• Inside the Kit
• Where to get help and to report bugs?

What is the Model-Checking Kit?

The Model-Checking Kit is a collection of programs which allow to model a finite-state system using a variety of modelling languages, and verify it using a variety of checkers, including deadlock-checkers, reachability-checkers, and model-checkers for the temporal logics CTL and LTL. The most interesting feature of the Kit is that

The counterexamples produced by the checker are presented to the user in terms of the description language used to model the system.

The Kit is an open system, and we expect that new description languages and checkers will be added in future. The current version of the Kit allows the user to model with:

• Automata communicating through shared variables and/or through channels.
• (1-safe Place/Transition) Petri nets.

• Clever explicit construction of the state space.
• Construction of a compact representation of the state space.
  • Binary Decision Diagrams.
  • Unfoldings.
• Construction of a reduced state space.
  • Stubborn sets.

The Kit in a nutshell

The Kit works as follows. Once it has been installed, you can model a system in one of the available modelling languages, and store it in a textfile system.txt.

To check deadlock-freedom, you type

where ml is one of the available modelling languages, and dc is one of the available deadlock-checkers. The Kit returns a deadlocking execution sequence if there is any.

To check if there is a reachable state satisfying a simple property, formalise the property in the state description language (more precisely, in the dialect of the state description language matching the modelling language of your choice) and store it in a textfile property.txt. Then type

where rc is one of the available reachability-checkers. The Kit returns an execution sequence leading to a state satisfying the property if there is any.

To check a temporal property, formalise it in CTL or LTL (more precisely, in the dialect of CTL or LTL matching the modelling language of your choice) and store it in a textfile property.txt. Then type

where mc is one of the available model-checkers. (The model-checker should correspond to your choice of temporal property.) The Kit returns an execution sequence violating the property if there is any.

That's it. If you want to see how this looks when applied to an example (Dekker's mutual exclusion algorithm), visit A sample session.

Why a Kit?

Research on automatic verification has shown that no single model-checking technique has the edge over all others in any application area. Moreover, it is very difficult to determine a priori which technique is the most suitable for a given model. It is thus sensible to apply different techniques to the same model. However, this is a very tedious and time-consuming task, since each algorithm uses its own description language. The Kit has been designed to provide a solution to this problem in an academic setting, with potential applications to industrial settings.

Intended users

The Model-Checking Kit has been

• primarily designed to be used by students in lab courses on automatic verification. Instructors cannot spend much time introducing the description languages of different tools, and students are unwilling to spend much time learning to use (often poorly documented) user interfaces.
• secondarily designed to help researchers to compare different model-checking techniques. Notice however that the verification times cannot be taken at face value, since the different checkers have been designed to work with different modelling languages. Still, we think that a comparison using the Kit can provide interesting information.

The Kit's Strengths

The Kit has been designed to be:

• Easy-to-use and easy-to-install
  Our experiments with beta-testers show that a moderately skilled user can install the tool and verify the first property of a small system within half an hour.
• Portable
  All the programs of the Kit are written in plain C. The source code of the Glue, the program holding the parts of the Kit together, can be found here. The source code of some of the Kit's checkers is also available.
• Open
  The Kit is an open library. Special care has been taken to make it modular. It is very easy to add new description languages or checkers, and to replace old versions by new ones. If you are interested in contributing to the Kit, see Making additions. We'll help you to solve the technical problems.

The Kit's weaknesses

In order to increase portability we do not offer any graphical interface: The Kit communicates with the user only through textfiles.

The Kit doesn't offer much help for checking that the model was correctly typed, and no help at all for many important steps of the design cycle, like for instance version maintenance.

Many of the Kit's checkers have been optimised for a particular modelling language, and translations can lead to losses in performance. Therefore, performance comparisons must always be taken with a grain of salt.

Which description languages can I use?

The current version of the Kit contains the following modelling languages (the keywords used by the Kit are in boldface).

• apnn. (Abstract Petri Net Notation.)
  A language for the description of different classes of Petri nets. Keywords are similar to LaTeX commands. An introduction to this language (postcript-file) can be found here.
• bpn2. (B(PN)² - Basic Petri Net Notation)
  A structured parallel programming language, offering among others loops, blocks and procedures.
• cfa. (Communicating Finite Automata).
  A language for the description of finite automata communicating through shared variables or through channels of finite length. cfa offers very flexible communication mechanisms. It is one of the modelling languages of the PEP tool.
• if. (Interchange Format).
  A language proposed in order to model asynchronous communicating real-time systems.
• pep. (Low level PEP notation.)
  A low level language, to be used by machines. It is included in this list only because some tools can export models in this language.
• senil. (Simple Extensible Net Input Language.)
  Another language for the description of 1-safe Place/Transition Petri nets. Suitable for small nets having at most some dozens of nodes, but not for larger projects. Designed to be used by students.

WARNING: The current version of the Kit can only work with 1-safe Petri nets (nets in which every reachable marking puts at most one token in a place). The net languages apnn, pep, and senil have to be used with care: if the input is a syntactically correct but not 1-safe net, the Kit doesn't protest, and may return nonsensical results. It is the user's responsibility to check that the input is indeed 1-safe.

The following languages may be added to the Kit in the future:

• A subset of SDL.

Which checkers can I use?

The current version of the Kit contains the following checkers (the keywords used by the Kit are in boldface):

• Grouped by the tool of origin.
• Grouped by functionality.
• Grouped by methods

Grouped by the tool of origin

• CLP . CLP is a linear programming model checker. It uses a finite complete prefix of a Petri net and can check deadlock freeness, reachability or coverability of a marking, or performs an extended reachability analysis, i.e. checks if there exists a marking satisfying the given predicate. CLP is distributed by the School of Computing Science, University of Newcastle upon Tyne.
  CLP contributes to the Kit:
  • A deadlock-checker: clp-dl.
• DSSZ . DSSZ is distributed by the Data Structures and Software Dependability Group of the Brandenburg Technical University at Cottbus. The package contains symbolic model checkers for safe (1-bounded) Petri nets using ZBDDs (Zero-suppressed Binary Decision Diagrams).
  DSSZ contributes to the Kit:
  • A CTL-checker: dssz-ctl.
    
  • A model-checker for LTL: dssz-ltl.
    These checkers were integrated by Alexey Tovchigrechko.
• LoLA . LoLA: LoLA is an explicit state space verification tool featuring partial order reduction (stubborn sets), the symmetry method, the sweep-line method, and several other reduction techniques. It has specialised versions of partial order reduction for many small classes of properties. LoLA is distributed by the Theory of Programming group at Humboldt-Universität zu Berlin.
  LoLA contributes to the Kit:
  • A CTL checker: lola-ctl.
    
  • A deadlock checker: lola-dl.
    
  • A reachability checker: lola-reach.
    
  In fact, the deadlock and reachability checkers come in five different flavours. See the file doc/lola/loladoku.txt in your downloaded package to learn more. These checkers were integrated by Karsten Schmidt.
• Mcsmodels. The tool mcsmodels is a model checker for finite complete prefixes (i.e. net unfoldings). It currently uses the PEP tool to generate the prefixes. These prefixes are then translated into logic programs with stable model semantics, and the integrated smodels solver is used to solve the generated problems. Mcsmodels is distributed by the Formal Methods and Logic Groups of the Laboratory for Theoretical Computer Science at the Helsinki University of Technology.
  Mcsmodels contributes to the Kit:
  • A deadlock-checker: mcs-dl.
  • A reachability-checker: mcs-reach.
• PEP. The PEP tool (Programming Environment based on Petri nets) is a programming and verification environment for parallel programs written in B(PN)² (Basic Petri Net Programming Notation), a powerful parallel, imperative programming language. B(PN)² has a formal Petri net semantics. Programs can be formally analysed using verification techniques based on the unfolding technique. PEP is distributed by the Theory group (subgroup Parallel Systems) of the University of Oldenburg.
  PEP contributes to the Kit:
  • A deadlock-checker: pep-dl.
  • A reachability-checker: pep-reach.
  • A model-checker for the next-free fragment of LTL: pep-ltl.
  Remark: Currently the reachability-checker and the LTL-model-checker are not integrated in the PEP tool, but they are based on the same techniques like the algorithms integrated in PEP.
• PROD. PROD is an advanced tool for efficient reachability analysis. It implements different advanced reachability techniques for palliating the state explosion problem, including partial-order techniques like stubborn sets and sleep sets, and techniques exploiting symmetries. PROD is distributed by the Formal Methods Group of the Laboratory for Theoretical Computer Science at the Helsinki University of Technology.
  PROD contributes to the Kit:
  • A deadlock-checker: prod-dl.
  • A reachability-checker: prod-reach.
  • A model-checker for the next-free fragment of LTL: prod-ltl.
  • A CTL model-checker: prod-ctl.
• SMV. The SMV system is a tool for checking finite state systems against specifications in the temporal logic CTL. The input language of SMV is designed to allow the description of finite state systems that range from completely synchronous to completely asynchronous, and from the detailed to the abstract.
  SMV contributes to the Kit:
  • A CTL model-checker: smv-ctl.
  • A deadlock-checker: smv-dl.
• SPIN . Spin is a widely distributed software package that supports the formal verification of distributed systems. Spin can be used as a full LTL model checking system, supporting all correctness requirements expressible in linear time temporal logic, but it can also be used as an efficient on-the-fly verifier for more basic safety and liveness properties. Many of the latter properties can be expressed, and verified, without the use of LTL.
  SPIN contributes to the Kit:
  • A model-checker for the next-free fragment of LTL: spin-ltl
    This checker was integrated by Ming Juan Qin.
    
  • A reachability checker: spin-reach
    

Grouped by functionality

• Deadlock-checkers.
  • prod-dl, smv-dl, mcs-dl, pep-dl, clp-dl, lola-dl.
• Reachability-checkers.
  • mcs-reach, pep-reach, prod-reach, lola-reach, spin-reach.
• Model-checkers.
  • CTL model-checkers: lola-ctl, prod-ctl, smv-ctl, dssz-ctl.
  • LTL model-checkers: prod-ltl, pep-ltl, spin-ltl, dssz-ltl.

Grouped by methods

• Explicit construction of the state space.
  This is the classical technique, and still the most adequate in many cases when the state explosion problem is not very acute.
  The Kit's checkers based on this technique are:
  • prod-ctl, spin-ltl, spin-reach.
• Stubborn set techniques.
  The stubborn set technique exploits information about the concurrency of actions to avoid constructing part of the state space. The states that are removed depend on the property to be checked. Stubborn sets were introduced by Antti Valmari in a number of papers.
  The Kit's checkers based on the stubborn set technique are:
  • prod-dl, prod-reach, prod-ltl.
  • lola-dl, lola-reach, lola-ctl.
• Symbolic techniques
  Symbolic techniques are used to succintly represent large (even infinite) set of states. Many different mathematical devices can be used. The most popular are Binary Decision Diagrams (BDDs), a data structure for boolean functions. BDDs can reach spectacular compactification ratios when the state space has a very regular structure.
  The Kit's checkers based on BDDs are:
  • smv-dl, smv-ctl, dssz-ctl, dssz-ltl.
• Unfolding techniques.
  The unfolding technique has been called ``the only truly partial-order technique''. A partial-order semantics of the system (an unfolding) is explicitely constructed and stored. The unfolding contains information not only on the reachability relation, but also on causality and concurrency. However, the checkers of the Kit do not use this extra information; they just exploit the fact that the reachability relation of concurrent systems is represented by the unfolding in a very compact way. The technique is thus adequate for systems exhibiting a high degree of concurrency.
  The unfolding technique was first described by Ken McMillan in his Ph.D. Thesis. An introduction to the technique can be found here, including a complete bibliography.
  The Kit's checkers based on the unfolding technique are:
  • mcs-dl, pep-dl, clp-dl, mcs-reach, pep-reach, pep-ltl.
  The pep and mcsmodels checkers differ in the methods used to extract information once the unfolding has been constructed. PEP's checkers use graph-theoretic algorithms and linear programming, while mcsmodels-checkers use logic programming with stable model semantics.

Inside the Kit

The Kit is held together by a program called the Glue. Given a system and a property modelled in one of the description languages supported by the Kit, the Glue

• Translates them into a 1-safe Petri net and a property of the net, described both in a common internal representation language.
• Translates the net and the property into input for the target model checker.
• Collects the output of the checker and translates it back into the original description language.

Why 1-safe Petri nets as internal representation?

• They are a very simple model with nearly no variants.
• They are a low level, unstructured model, which can simulate different communication disciplines, both synchronous and asynchronous.
• They have a very simple notion of ``independent actions'', and are so a very adequate model for partial-order model-checking techniques.
• They have a very simple notion of state (a vector of booleans), which makes them also very adequate for symbolic methods.

Where to get help and to report bugs

Next chapter: News