Marrella Demo

Marrella and the Verification of an Embedded System

Dominique Ambroise, Patrick Auge (Université de Paris Sud),
Kamel Bouchefra (Université Paris 13),
Brigitte Rozoy (Université de Paris Sud)

We present the architecture of Marrella, a tool designed for simulation and verification of distributed systems. The input of the tool is an event driven language whereas the underlying model is event-structures. It gives the possibilities of generating one, some or all the executions of any distributed program. We have tested the tool for the verification of an embedded system. The results are reported there, as well as comparison with other known tools applied to the same case study.