## Model-Checking Kit

** Category** Cross-Omics>Agent-Based Modeling/Simulation/Tools

** Abstract** The Model-Checking Kit is a collection of programs which allows you to model a finite-state system using a variety of Modeling languages (see below...), and verify it using a variety of Checkers (see below...), including deadlock-checkers, reachability-checkers, and model-checkers for the temporal logics CTL (Computational tree logic) and LTL (Linear temporal logic).

The most interesting feature of the Model-Checking Kit according to the manufacturers is that - Independently of the description language chosen by the user, (almost) all checkers can be applied to the same model.

The counter examples 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 the manufacturers expect that new description languages and checkers will be added in future.

The current version of the Kit allows the user to model with:

1) Automata communicating through shared variables and/or through channels.

2) (1-safe Place/Transition) Petri nets.

The checkers make use of state-of-the-art techniques to palliate the state-explosion problem, including:

1) Clever explicit construction of the state space.

2) Construction of a compact representation of the state space.

- a) Binary Decision Diagrams
- b) Unfoldings.

3) Construction of a reduced state space.

- a) Stubborn sets.

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.

Model-Checking Kit Intended users --

The Model-Checking Kit has been:

1) 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.

2) Secondarily designed to help researchers to compare different model-checking techniques. Note however, that the verification times cannot be taken at face value, since the different checkers have been designed to work with different modeling languages. Still, the manufacturers think that a comparison using the Kit can provide interesting information.

Modeling languages --

The current version of the Kit contains the following modeling languages:

1) apnn (Abstract Petri Net Notation) - A language for the description of different classes of Petri nets. Its keywords are similar to LaTeX commands.

2) bpn2 [B(PN) to the second power - Basic Petri Net Notation] - A structured parallel programming language, offering among other features; loops, blocks and procedures.

3) 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 modeling languages of the PEP tool (see G6G Abstract Number 20609).

4) if (Interchange Format) - A language proposed in order to model asynchronous communicating real-time systems.

5) 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.

6) 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 dozens of nodes, but Not for larger projects. It is designed to be used by students.

Note: 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 a 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.

Checkers - Grouped by the tool of origin --

1) 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) A deadlock-checker: clp-dl.

2) 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) A CTL-checker: dssz-ctl.
- b) A model-checker for LTL: dssz-ltl. These checkers were integrated by Alexey Tovchigrechko.

3) 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 specialized 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) A CTL checker: lola-ctl;
- b) A deadlock checker: lola-dl; and
- c) A reachability checker: lola-reach.
- In fact, the deadlock and reachability checkers come in five (5) different flavors. These checkers were integrated by Karsten Schmidt.

4) 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) A deadlock-checker: mcs-dl.
- b) A reachability-checker: mcs-reach.

5) PEP - The PEP tool (Programming Environment based on Petri nets) is a programming and verification environment for parallel programs written in B(PN) to the second power (Basic Petri Net Programming Notation), an advanced parallel, imperative programming language. B(PN) to the second power contains formal Petri net semantics.

Programs can be formally analyzed 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) A deadlock-checker: pep-dl;
- b) A reachability-checker: pep-reach; and
- c) A model-checker for the next-free fragment of LTL: pep-ltl.

Note: Currently the reachability-checker and the LTL-model-checker are Not integrated in the PEP tool, but they are based on the same techniques as the algorithms integrated in PEP.

6) 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 such as, 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) A deadlock-checker: prod-dl;
- b) A reachability-checker: prod-reach;
- c) A model-checker for the next-free fragment of LTL: prod-ltl; and
- d) A CTL model-checker: prod-ctl.

7) 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) A CTL model-checker: smv-ctl.
- b) A deadlock-checker: smv-dl.

8) 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) A model-checker for the next-free fragment of LTL: spin-ltl. This checker was integrated by Ming Juan Qin.
- b) A reachability checker: spin-reach.

*System Requirements*

Contact manufacturer.

*Manufacturer*

- Institute of Formal Methods in Computer Science
- University of Stuttgart
- Universitätsstr. 38
- 70569 Stuttgart, Germany

** Manufacturer Web Site**
Model-Checking Kit

** Price** Contact manufacturer.

** G6G Abstract Number** 20638

** G6G Manufacturer Number** 104237