POP, A Polychronous Modeling Environment on Polarsys
The Polychrony project is a proposed open source project under the Polarsys Top-Level Project, which is operating under the auspices of the Polarsys Industry Working Group.
This proposal is in the Project Proposal Phase (as defined in the Eclipse Development Process) and is written to declare its intent and scope. We solicit additional participation and input from the Eclipse community. Please send all feedback to the Eclipse Proposals Forum.
Scope
The Eclipse Polychrony project provides a Signal Integrated Development Environment based on the Eclipse platform (Signal is a specification and programing language for critical/real-time embedded applications).
This project, also referred to as SSME platform, includes the meta-model of Signal under Eclipse (SSME), a reflexive editor, a code editor with syntax highlighting, an Eclipse view to create compilation scenarios, the import of some other formalisms (aadl, Geneauto/simulink).
It provides access to the other elements of the whole Polychrony Toolset (see figure):
- The Signal Toolbox, a batch compiler for the Signal language (command line out of Eclipse), and a structured API that provides a set of program transformations. It can be installed without the other components.
- The Signal GUI, a graphical user interface to the Signal Toolbox (editor + interactive access to compiling functionalities of the Signal ToolBox). It requires the Signal Toolbox. It can be used as Signal GUI editor under Eclipse.
Description
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.
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.Relationship with Eclipse Projects
The Polychrony plug-ins under Eclipse suite is composed of several plug-ins which correspond to: the reflexive editor and an Eclipse view to create compilation scenarios, and the connection to the Polychrony Signal ToolBox services. The reflexive editor is the plug-in generated by the Eclipse Modeling Framework (EMF) from the meta-model of Signal (SSME).
Moreover, the import of the AADL formalism requires the Osate Eclipse plug-ins and the Eclipse plug-ins developed for the standardized Behavior Model Annex of AADL (see Telecom ParisTech AADL corner). It requires the Eclipse Xtext project.
Why Polarsys?
Polychrony is an environment for the definition of critical/embedded systems. The use of the formal methods implemented in Polychrony may be useful to Polarsys community because formal design frameworks provide well-defined mathematical models that yield a rigorous methodological support for the trusted design, automatic validation, and systematic test-case generation of systems.
Our goal is to generalize the use of formal methods implemented in Polychrony by making them accessible in more popular framework, used by thousands of users and companies.
Initial Contribution
There will be an initial contribution of Polychrony toolset: Polychrony has been integrated under the experimental Polarsys platform during the OPEES project. This integration of Polychrony under this platform has been realized in collaboration with the CS company.
CS and INRIA have produced the Polychrony experimentation report which is included in the global experimentation report. For the qualification of the Polychrony component on the Polarsys platform, CS and INRIA provide the following documents:
- The Tool Quality Assurance Plan Template (TQAP). This document defines the OPEES quality assurance arrangements and gives some guidance to satisfy them. It focuses on qualification aspects and gives in appendices guidance for some criteria tool qualification with an example for Polychrony Tool.
- The Tool Verification Cases and Procedures (TVCP) document. It presents the tests cases to be performed for the qualification of Polarsys Polychrony Verifier component as described in the TQAP.
- The Tool Verification Results (TVR). It presents the results of tests performed for the qualification of Polychrony Verifier on several operating systems, as described in the TQAP.
Legal Issues
The SSME platform and the AADL to Signal translator are under Eclipse Public License. The Signal toolbox and the Signal GUI are under GPL-V2 license. So, the source of the Signal Toolbox and the Signal GUI will not be under the Polarsys repository. It is available on the Espresso web site.
The Signal Toolbox is an Eclipse feature. This feature is composed of a set of plugins in which fragments are defined (operating system and architecture dependent). Such a plug-in provides the Signal ToolBox as an external dynamical library because the Eclipse Polychrony calls interactively the functionalities of the Signal ToolBox. This feature is also available on the update site of the Espresso web site.
Committers
The following individuals are proposed as initial committers to the project:
- Loïc Besnard, CNRS
- Loïc Besnard is part of the Polychrony development team for several years. He will provide the implementation of the transformations applied to a Signal program defined in the Signal toolbox, the SSME platform, and the inter-format translators.
- Thierry Gautier, INRIA
- Thierry Gautier has provided significant contributions to the existing code base and the definition of the Signal Syntax. He will contribute to the evolution of the Signal language (a new version is scheduled in 2013).
- Paul Le Guernic, INRIA
- Paul Le Guernic has designed the Signal language. It has provided significant contributions to the existing code base and the definition of the Signal Syntax. He will contribute to the evolution of the Signal language.
We welcome additional committers and contributions.
Project Leads
- Jean-Pierre Talpin, INRIA
- Dr. Jean-Pierre Talpin is Directeur de Recherche at INRIA and, since 2000, scientific leader of INRIA project-team Espresso, comprising 4 full-time researchers and between 10-15 members in total. Jean-Pierre Talpin received a Ph.D. Degree in Computer Science (1993) from the University of Paris VI Pierre et Marie Curie for the Thesis he prepared at Ecole des Mines de Paris. He worked as Research Associate at the European Computer-Industry Research in Munich before to join INRIA in 1995. He served eight years as elected member of INRIA's evaluation commission (2002-2009). He coordinated OpenEmbeDD, the first ANR platform project, from 2006 to 2009, which was commended as leading project at its final evaluation and continued with the ITEA2 project OPEES, where he served as work-package leader. Jean-Pierre Talpin is co-editor of two scientific books and fourteen special issues of international scientific journals and conference proceedings. He co-authored more than ninety book chapters, scientific journal articles and international conference papers. In 2005, he received the ACM SIGPLAN Award of the most influential POPL paper for his article with Mads Tofte presented at POPL'94. In 2012, he received the ACM/IEEE LICS Test-of-Time Award for his LICS'92 article with Pierre Jouvelot.
Mentors
The following Architecture Council members will mentor this project:
- Naci Dai
- Michael Scharf
- Cedric Brun
Interested Parties
The following individuals, organisations, companies and projects have expressed interest in this project:
- Airbus
- Brest University
- CS
- Ellidiss Technologies
- INRIA, Aoste Team
- Kaiserslautern University, Embedded system group
- Rennes University
- RockwellCollins France
- Shenzhen Institutes of Advanced Technology of China
- Topcased community
- Virginia Tech., Fermat laboratory
Project Scheduling
As said before, Polychrony has been integrated in the experimental Polarsys platform. The first build is ready for the following platforms: Windows (32-64 bits), Linux (32-64 bits), and MacOS.Polychrony project scheduling will be aligned on the planning of the Polarsys 3P proposal:
- April 2013: releasing PolarSys IDE milestone 1.0M1
- July 2013: releasing PolarSys IDE milesonte 1.0M2
- Oct 2013: PolarSys IDE 1.0, aligned on Kepler, platforms: Windows (64 bits), Linux (64 bits), MAC, Solaris
Changes to this Document
| Date | Change |
|---|---|
| 11-Sept-2013 | Proposed project named changed to "POP, A Polychronous Modeling Environment on Polarsys" |