| Partner Institutions |
| Persons involved in the project |
| Scientific Results |
Publications, software and formal developments
| Short Summary |
The project proposed here aims at substantially improving the safety and reliability of embedded software that is being developed in the context of a Model Driven Engineering approach. This is achieved by formally proving the correctness of essential transformations that a model undergoes during its compilation to executable code.
The project is targeted at the compilation of a synchronous language to an imperative programming language. Synchronous languages have turned out to be an expressive formalism for embedded algorithms, and their precise semantics make them particularly suitable for our purpose. We plan to extend the core formalism with quantitative timing information, which is taken into account by the transformations, so as to make the approach viable for the development of real-time systems.
The definition of the semantics and the correctness proof of the compiler will be carried out in the interactive proof assistant Isabelle. The compiler is executable and will be evaluated on realistic examples.
This project is foundational in that its results are not a standalone product which is immediately usable in an industrial context. However, the motivation for this project has emanated from projects with major players of the embedded sector that the partners are involved in, and the results will be fed back to projects of industrial relevance.
| Last modified: Sat Jul 20 12:02:50 CEST 2013 |