Eclipse Formal Modeling Project

The general purpose of E-FMP project is to develop a series of formal analysis tools and enable a broader use of them thanks to their integration with the Eclipse modeling technologies. The first tool to be provided by the E-FMP project is a symbolic execution platform. In the following, we define precisely the scope this platform. 

The first objective of the symbolic execution platform of the E-FMP project is to provide researchers with a common platform :

• generic enough to take into account all the objects they want to analyze;
• extensible in order to allow them to customize the basic symbolic treatments to implement their specific formal functionalities.

Offering such functionalities will enable the share and the coordination of different researches that will be implemented in a common symbolic platform. This will permit using conjointly different formal techniques in a common framework. Moreover, from the contributors’ perspective, they do not have to re-implementing basic symbolic execution functionalities. Rather, they are expected to concentrate on the formal usage that they want to make of them.

The second objective of the symbolic execution platform of the E-FMP project is to provide users with user-friendly formal functionalities:

This will be made possible thanks to a catalogue of import and export gateways that will be developed all along the project life. At the beginning of the project, the import gateway from UML/SysML will be released and enriched. The export gateway to TTCN-3 will be also released.