The Model-Checking Kit

Overview

Entry last updated: 2003/5/2
Entry last validated: 2004/5/18

Tool homepage: http://www.informatik.uni-stuttgart.de/fmi/szs/tools/mckit/

Tool availability: Free of charge

Tool Features

Petri Nets Supported (see also help on terminology)

High-level Petri Nets
Place/Transition Nets

Components (see also help on terminology)

State Spaces
Condensed State Spaces
CTL-/LTL-Model-Checking, Deadlock-Checking, Reachability-Checking

Environments

Sun
Linux

Tool Description

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 checkers are taken from different existing tools like PROD, SMV, or PEP. They use state-of-the-art techniques to avoid the state explosion problem, such as symbolic model checking (BDDs) and partial orders. The modelling languages include among others the low level language of PEP, because some tools can export models to this language, B(PN)², a structured parallel programming language and CFA, a language for the description of communicating finite automata.

The most interesting feature of the Kit is that independently of the description language chosen by the user all checkers can be applied to the same model. It is not necessary to model the system in different modelling languages.

Contact Information

Prof. Dr. Javier Esparza
Universit„t Stuttgart
Institut f’r Formale Methoden der Informatik
Abteilung Sichere und Zuverl„ssige Softwaresysteme
Universit„tsstr. 38
D-70569 Stuttgart
Germany

Phone:  +49 711 7816-455
Fax:    
E-mail: mckit@in.tum.de

Other Remarks

The maintainers of this page