Task T2.2: Integration of tools

1. The tools LASH and TReX which are developed in the project are interfaced with the IF environment. These tools can handle extended automata written in IF, more precisely, automata communicating through shared variables or unbounded FIFO queues, equipped with variables ranging over the following types: booleans, enumerate types, clocks, and unbounded integer counters.
2. The group of Edinburgh is developing a specification and verification environment called the Model Checking Kit (MCK). It consists of 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.
3. An interface between the MCK and the common description language IF has been implemented. It includes 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.