The complexity of large distributed systems is a problem when designers want to evaluate their properties. Systematic tests of the application cannot be considered as verification because of the parallelism.

Researches in this area do outline the need for a modeling step. Modeling produces a set of views about a system that are usefull for evaluation, validation, verification and also code generation. These activities may be grouped under the word «prototyping». Prototyping does not designate only program generation techniques. It is now accepted as an apporach to the implementation of systems involving modelling, validation and verification as well as program generation.

Formalisms such as Colored Petri nets are now widely used for the formal modeling of parallel systems. However, their main drawback is their poor structuring facilities. They are thus difficult to use for large scale systems. To compensate lack of structuration, two research strategies are usually considered:

• The integration of new high level features, as hierarchy [Buchholz 94] enables modeling of more complex systems but raises theoretical problems. Some properties can no longer be computed. Not all properties extractable from non hierarchical nets can be computed either;
• The association between Petri nets and another high level representation enbales the use of its structuring capabilities [Di Giovanni 90, Sibertin-Blanc 94, Lakos 95]. The idea is to produce a flat Petri net from a semi-formal model. The Petri net specification should be huge but is hidden to the end user. Properties of this model must be translated back in the terms of the high level formalism.

The Mars project considers the second strategy. It aims at the encapsulation of Petri nets to make them usable by engineers having a very little knowledge concerning formal methods and Petri nets. The objectif is to produce an object oriented high level language suitable for the modelling of large systems and able to maintain a link with formal methods like Petri nets.

These concepts are associated to Petri nets in order to maintain verification capabilities and to help a non specialist designer to elaborate a system that has «good» properties (deadlock-free, proper use of software components, etc.). To do so, we focus on the modular design, validation and generation of large distributed systems.

To experiment our techniques on a large scale (on various problems issued from the industry or institution like CIRAD [Bakam 00]), we have elaborated CPN-AMI [Kordon 99b], a Petri net based CASE (Computer Aided Software Engineering) environment. To built it at reasonable costs and to be able to integrate work from university partners, we have designed FrameKit [Kordon 98], a generic integration platform and Macao, a generic user interface. Finally, to experiment program generation techniques, we have elaborated MetaScribe [Kordon 99a, Regep 00], a transfromation engine builder.

This project is a support for numerous experimentations and work around the design, formal analysis and implementation of distributed systems for several years. It was used in the context of many projects. Here is a list of :

• MATCH (Modeling and Analysis of Time Constrained and Hierarchical systems, ChrX-CT94-0452) from 1995 to 1998.
• CARISMA (CNET project) from 1997 to 1998.
• CaMoS (VAlidation MOdulaire de Systèmes, inside the formA action) from 1997 to 2000.
• cooperation with CIRAD/TERA to analyse agent systems for the management of hunting in Cameroon in 2000 and 2001.
• within the context of the MORSE project (RNTL program, 2003-2006). many aspects of the LfP language where experimented, even before this project (2001 to 2006).
• within the context of the PolyORB project since 2004, in particular, all the validation of the middleware kernel was performed with CPN-AMI.
• we are currenty using CPN-AMI to analyse strategies for Intelligent Transport Systems, in particular the behavior of vehicle-to-vehicle and vehicle-to-infrastructure interaction.

We do participate in the effort for the definition of the Petri Net standard (ISO/IEC-15909), in particular in the definition of the Stuctured Class Net class. CPN-AMI is also a testbench for a reference implementation of the PNML language.

You will find in this web site information about all the elements of the Mars project that are available on our web site.