Polychrony Qualification Kit
The POLYCHRONY TOOLSET provides a formal framework:
- to validate a design at different levels, by the way of formal verification and/or simulation
- to refine descriptions in a top-down approach,
- to abstract properties needed for black-box composition,
- to assemble heterogeneous predefined components (bottom-up with COTS).
- to generate executable code for various architectures
The POLYCHRONY TOOLSET, is an Open Source development environment for critical/embedded systems,based on SIGNAL, a real-time polychronous dataflow language ( see Polychrony web site). POLYCHRONY provides a unified model-driven environment to perform 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. It can be included in heterogeneous design systems with various input formalisms and output languages.
The POLYCHRONY TOOLSET contains three main components:
- The SSME (Signal Syntax Model under Eclipse) PLATFORM, a front-end to the SIGNAL TOOLBOX in the ECLIPSE environment. The SSME PLATFORM may be used to import other formalisms (AADL, Synoptic, Geneauto).
- The SIGNAL GUI, a Graphical User Interface to the SIGNAL TOOLBOX (editor + interactive access to compiling functionalities).
- The SIGNAL TOOLBOX, a batch compiler for the SIGNAL language, and a structured API that provides a set of program transformations. It also provides:
- libraries of SIGNAL programs,
- a set of SIGNAL programs examples,
- user oriented and implementation documentations,
- facilities to generate new versions.
SIGNAL (Polychrony web site) is a specification and programing language for critical/real-time embedded applications. The main features of the SIGNAL languages are
- synchronized flows (flows + synchronization) and
- processes: a process is (recursively) a set of equations over synchronized 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 mandatory to write partial specifications, to specify non-deterministic devices (for instance a non-deterministic bus), and to abstract the behavior of 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. More details can be found in a short introduction to SIGNAL language on the Polychrony web site.