Skip to content
 

Polychrony

Document Actions

Polychrony is an integrated development environment and technology demonstrator for computer-aided embedded software design. It is based on the synchronous multi-clocked (polychronous) model of computation implemented in the data-flow language Signal. The toolset consists of a compiler, a model checker and control synthesizer.

Polychrony is developed by the project-team Espresso, whose scientific objectives are to define and implement models, methods and tools for the computer-aided engineering of trusted application architectures in embedded and mission-critical software. Polychrony is free software available at http://www.irisa.fr/espresso/Polychrony

Polychrony is integrated with Eclipse by a plug-in which allows for the interactive, multi-view, modelling and edition interface, transformation, verification and visualisation interface, of high-level behavioural specifications consists of hybrid mode-automata and block diagrams.

Polychrony provides a unified model-driven design environment to perform embedded software design exploration from imported heterogeneous models by using correctness-preserving transformations. Its design methodology is formally supported by the polychromous model of computation to carry out design transformations from specification to implementation and from synchrony to asynchrony.

The company Geensys supplies a commercial implementation, RT-Builder, used for industrial scale projects by several large industrial groups (see http://www.tni-software.com).

polychrony_screenshot

Features

  • Unified model-driven design environment

    • Synchronous, multi-clocked, dataflow and mode automata specification language

    • Validation and verification with the SIGALI, SMV, CADP, Coq

  • Simulation of embedded software architectures

    • Model library for ARINC-653 services

    • Import of AADL specifications

  • Scriptable C, C++, Java code-generation strategies

    • Sequential, modular, distributed or clustered

    • Static or dynamic scheduling, OS and middleware-specific artefacts

  • Capability to interface and embed legacy C or interpret C functions in SSA form

  • Export towards scheduling tools to generate machine-specific real-time code

References