Primary tabs

Signal (Polychrony web site) is a specification and programming 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.

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 here.

The Polychrony Toolset, based on the Signal language, 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.

Polychrony offers services for modeling application programs and architectures starting from high-level and heterogeneous input notations and formalisms. These models are imported in Polychrony using the data-flow notation Signal. Polychrony operates these models by performing global transformations and optimizations on them (hierarchization of control, desynchronization protocol synthesis, separate compilation, clustering, abstraction) in order to deploy them on mission specific target architectures. C, C++, multi-threaded and SynDEx (a distribution tool) code generators are provided.

Sigali and Fiacre code generators for formal verifications are also provided.

Contribution Activity: 
Commits on this project (last 12 months).