The Model Checking Kit

The Model Checking Kit (MCK) is a collection of programs which allow to model a finite-state system using a variety of modeling 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, independently of the description language chosen by the user, (almost) all checkers can be applied to the same model. The checkers that are currently available include PEP, PROD, SMV, SPIN, and others.

We have implemented an interface between the common description language (IF) and the Kit. It includes a a compiler from IF into safe Petri Nets (the basic model of the Kit), a formula converter which translates properties of the original model into Petri net properties, and a trace interpreter which translates error traces of the Petri net back into traces of the original model. The fragment covered by the compiler excludes the real-time features of the language and is limited to finite data types (since these cannot be modeled in the target language), but includes important features like dynamic process creation or different signal delivery disciplines.

More precisely, the list of supported features is as follows:

• Systems consist of multiple processes running in parallel; multiple instances of a process can exist simultaneously, but the maximum number of concurrently active instances has to be fixed a priori.
• Processes can communicate by exchanging signals or through shared variables. Signals (which may take arguments) can pass either through signalroutes or through direct communication between processes. Incoming signals are stored in a message queue. A limitation is that the capacity of the message queue has to be fixed a priori.
• Signalroute can have different delivery disciplines in the common language most of which are supported by the compiler: FIFO and multiset queueing, reliable and lossy transmission, peer-to-peer, unicast, and multicast delivery. Moreover, the common language provides for urgent (immediate) and delayed delivery. In the case of delayed delivery, the language allows to place temporal constraints on the amount of delay and the transmission rate. These temporal restrictions are not supported by the compiler, but distinction is made between immediate and delayed delivery where signals are stored in a buffer (of fixed size).
• The following data types are supported by the compiler:
  • finite integer fragments
  • process/signalroute ids
  • booleans
  • enum and range types
  The following types are not supported
  • floats, clocks and unbounded integer types
  • arrays and records (though these could be added if necessary)
  • strings and abstract types
• Procedures (which are used to import C code into the system) are not supported.
• Of the guards that control entry into a state transition, we support the input and the provided guards. The temporal guards tpc, deadline, or when are not supported. Save sets are not currently supported, but can be considered for implementation if needed.
• Of the actions available inside state transitions, we support manipulation of variables (task), sending of signals (output), and the dynamic creation of processes (complete with the passing of arguments) and signalroutes, as well as process/signalroute destruction (kill). Actions to do with clocks (set/reset) are not supported.