The Polychrony toolset, the Signal language, the SSME environment and the AADL to SIGNAL translator have been designed at IRISA as a technology demonstrator for the research activities of the ESPRESSO and TEA projects and its academic or industrial partners. It is distributed and maintained by INRIA project-team TEA on the platform of the Polarsys Industry Working Group, project POP (Polychrony on Polarsys).

The Polychrony Toolset

Polychrony is an integrated development environment and technology demonstrator. It provides a unified model-driven environment to perform embedded system design exploration by using top-down and bottom-up design methodologies formally supported by design model transformations from specification to implementation and from synchrony to asynchrony.

The Polychrony toolset, based on Signal, provides a formal framework:

• to validate a design at different levels,
• to refine descriptions in a top-down approach,
• to abstract properties needed for black-box composition,
• to assemble predefined components (bottom-up with COTS).

The principle application areas for the Signal language are that of embedded, real-time, critical systems. Typical domains include:

• Process control,
• Signal processing systems,
• Avionics,
• Automotive control,
• Vehicle control systems,
• Nuclear power control systems,
• Defense systems,
• Radar systems.

It constitutes a development environment for critical systems, from abstract specification until deployment on distributed systems. It relies on the application of formal methods, allowed by the representation of a system, at the different steps of its development, in the Signal polychronous semantic model.

Based on the same polychronous principles, there is a commercial tool, RT-Builder, provided by the Geensoft company (Dassault Systèmes).

Polychrony is a set of tools composed of:

• A Signal batch compiler providing a set of functionalities viewed as a set of services for, e.g., program transformations, optimizations, formal verification, abstraction, separate compilation, mapping, code generation, simulation, temporal profiling...
• A Graphical User Interface (editor + interactive access to compiling functionalities)
  Warning: This GUI is a temporary one. A new version is currently being developed. It cannot be guaranteed that the graphical representation of Signal programs developed with the current GUI will be compatible with that of the new GUI.
• The Sigali tool, an associated formal system for formal verification and controller synthesis. Sigali is developed together with the Vertecs project. More documentation about Sigali can be found here.

The Signal language

Signal is based on synchronized data-flow (flows + synchronization): a process is a set of equations on elementary flows describing both data and control.

The Signal formal model provides the capability to describe systems with several clocks (polychronous systems) as relational specifications. Relations are useful as partial specifications and as specifications of non-deterministic devices (for instance a non-deterministic bus) or external processes (for instance an unsafe car driver).

Using Signal allows to specify an application, to design an architecture, to refine detailed components downto RTOS or hardware description. The Signal model supports a design methodology which goes from specification to implementation, from abstraction to concretization, from synchrony to asynchrony.

A short introduction to Signal can be found here.

The SME environment

The SME environment is a front-end of Polychrony in the Eclipse environment based on Model-Driven Engineering (MDE) technologies. It consists of a set of Eclipse plug-ins which rely on the Eclipse Modeling Framework (EMF). The environment is built around SME, a metamodel of the Signal language extended with mode automata concepts.

The SME environment is composed of several plug-ins which correspond to:

• A reflexive editor: a tree view allowing to manipulate models conform to the SME metamodel.
• A graphical modeler based on the TopCased modeling facilities (cf. previous picture).
• A reflexive editor and an Eclipse view to create compilation scenarios.
• A direct connection to the Polychrony services (compilation, formal verification, etc).
• A documentation and model examples.