by Bernard Berthomieu, Hubert Garavel, Frédéric Lang and François Vernadat
The TOPCASED project (Toolkit in Open source for Critical Applications and SystEm Development) of Aerospace Valley ('Pôle de compétitivité' in aerospace activities) has developed an extensible toolbox that provides graphical environments for mission-critical systems engineering. Within this project, the FIACRE intermediate format allows the connection of several graphical models to verification tools such as CADP and TINA, as well as the factoring of expensive developments.
Mission-critical systems, such as embedded systems, aeronautic systems, computer architectures or systems on chip, are becoming increasingly complex. To tackle this complexity, systems are often designed as components that execute concurrently and communicate with one another. Models of these components can be drawn using graphical environments and then transformed into executable code.
Components can be modelled using various graphical languages: these can be either generic, such as UML, or specific to an application domain, such as DSLs (Domain Specific Languages). Since developing dedicated tools for each language would be too expensive, it is desirable wherever possible to employ tool developments that can be reused for several languages. This is the goal of meta-modelling.
TOPCASED is a project of Aerospace Valley ('Pôle de compétitivité' in aerospace activities). Led by Airbus, TOPCASED involves 36 partners from both research (CNES, ENSEEIHT, ENSIETA, ESEO, INRIA, IRIT, LAAS-CNRS, ONERA, etc) and industry (AdaCore, AnyWare Technologies, ATOS Origin, Communication & Systems, Continental, EADS-Astrium, Rockwell & Collins, SodiFrance, Sogeti-HiTech, Sopra Group, Thales Avionics, TurboMeca, TNI-Software, etc). TOPCASED has used a meta-modelling approach to develop an open source environment based on Eclipse. Release 2.0.0 of the TOPCASED environment (18 July 2008) provides graphical tools for several languages, including UML, SysML, SAM and AADL. Its editors are already in use for several industrial projects. The software components developed in TOPCASED are integrated with the French national platform OPENEMBEDD.
As malfunctions in critical systems may have severe human or economic consequences, guaranteeing behavioural requirements and real-time constraints is a great challenge for companies. Such requirements include dynamic properties such as absence of deadlocks, safety properties (guaranteeing that unexpected events will not happen in the system) and liveness properties (guaranteeing that expected events will eventually happen in the system). Model checking tools have been developed for this. Since model-checking tools are expensive, it would be unrealistic to develop a dedicated tool for each language supported by TOPCASED. For this reason, we found it necessary to develop a common intermediate format into which all languages converge using transformations.
This intermediate format, named FIACRE ('Format Intermédiaire pour les Architectures de Composants Répartis Embarqués'), was developed within several projects including TOPCASED and OPENEMBEDD. FIACRE is based upon the NTIF format ('New Technology Intermediate Form') developed at INRIA, and the COTRE language ('Composants Temps Réel') developed within the COTRE RNTL project.
It consists of an extension of usual state machines with a rich notion of transitions borrowed from NTIF, which allows large pieces of sequential code to be embedded in each transition, resulting in compact models and an easy mapping from real languages and large applications. On top of these machines, a layer of components inspired by COTRE allows these communicating state machines to be hierarchically composed and real-time constraints to be specified. Rich behaviours can be expressed in a compositional way.
Several teams are developing transformations from graphical languages into FIACRE: transformations from AADL and SDL have been specified by IRIT and Communication & Systems, and a transformation from Signal/Polychrony has been developed at INRIA Rennes .
FIACRE is also connected to model checkers using two transformation tools. First, FLAC (Fiacre to LOTOS Adaptation Component) translates FIACRE programs into LOTOS (an ISO standard for concurrent systems specifications), which can be later checked using CADP, a verification toolbox used by the hardware industry to verify high-performance processors and architectures. Second, FRAC (FiacRe to tinA Compiler) translates FIACRE programs into the input language of the TINA toolbox (Time Petri Net Analyser, http://www.laas.fr/tina), which may be used to check dynamic properties including real-time constraints on a family of models extending Time Petri nets.
Thus, the TOPCASED and OPENEMBEDD projects are building on the efforts of two communities, model-driven software engineering and computer-aided verification, to provide industry with development tools that integrate the recent results of these communities.
Links:
http://www.inrialpes.fr/vasy/cadp
http://www.laas.fr/tina
http://www.topcased.org
http://openembedd.inria.fr
Please contact:
Frédéric Lang
INRIA Grenoble Rhône-Alpes, France Tel: +33 4 76 61 55 11
E-mail: Frederic.Lang
inria.fr
