Languages and Tool-Chain for the Development of Safe Embedded Components |
Keywords
|
|
Abstract
This project addresses large size critical embedded systems, for which reuse is becoming crucial. The objective is to study an integrated development environment for the construction and use of safe embedded components. The use of an appropriate programming language being one of the key points contributing to safety in computer systems, we will favour a "language" approach for all the following aspects:- managing the whole life-cycle, from early specification phases to efficient embedded code;
- modular composition mechanisms, to be used as well for: programs, their specifications, the description of their environments;
- early validation while assembling components;
- early validation of the system's dynamic behaviour, based on simulations of programs and specifications, all along the life-cycle; executing incomplete programs is one of the key objectives.
The proposed approach consists in defining a set of languages, and their associated tools, on top of a common semantical basis.
We choose the synchronous mathematical model, which gives a clean and simple semantics to concurrency and time. It has been used successfully for the definition of languages and tools (e.g, Scade, Sildex, Esterel) dedicated to the development of critical control software. It already allows the description and composition of programs and properties in a common framework. It is general enough to describe other concurrency models (like asynchronism) and to combine deterministic and non-deterministic objects.
In this common framework we will define a set of languages for: programming, specifying programs and environments, assembling components, and the properties of the assembling structures.
On the other hand, we will study how to apply formal validation very early in the life-cycle, to the following aspects: validation of the assembling structures, validation of a component for a given environment, etc. We propose to express these new validation problems in terms of existing verification problems, and to plan a connection interface between our development environment and existing verification tools.
The project benefits from the competences of the research teams involved, concerning: synchronous languages and tools; semantics and implementation techniques for embedded software; validation and simulation tools for complex computer systems.
