The Modal Transition System Analyser

The Tool

MTSA is a prototype tool aimed at supporting the elaboration and verification of behaviour models for reactive systems. Modal Transition Systems allow partially describing the behaviour of a system and support through refinement the incremental elaboration of the model.

MTSA is built on top of LTSA. LTSA is the Labelled Transition System Analyser.

MTSA is an open source project written in Java. To download and run MTSA go to sourceforge. Unfortunately, we do not have any documentation for the tool. Please refer to the examples packaged with the tool or the papers.

The People

Contributors to the MTSA implementation are:

Dario Fischbein

Nicolas D'Ippolito

Sebastian Uchitel

Collaborators on the ideas, theory and algorithms involved include: Marsha Chechik and Greg Brunet.