Formal translation validation between synchronous data flow equations and application to a Lustre

Marc Pouzet

Description

Niveau: Supérieur, Doctorat, Bac+8
Formal translation validation between synchronous data-flow equations and application to a Lustre compiler Master 2 Internship November 2011 Level : M2R Length : 6 months (spring 2012) Advisor : Marc Pouzet () Location : Departement d'Informatique, Ecole Normale Superieure, 45 rue d'Ulm, 75230 Paris cedex 05. Prerequisite : This internship is for a student with strong interest and skills in functional program- ming, the use of the Coq proof environment, the semantics and implementation of programming languages and reactive systems. Collaboration : The work can be continued with a PhD. thesis, in the PARKAS group, in colla- boration with the SCADE team of Esterel-Technologies. Research Context The synchronous data-flow language SCADE 1 is used for implementing reactive systems in various critical domains such as nuclear energy, civil avionic, railways, etc. These uses have called for the “certification” of the C code generator of SCADE with the highest safety requirements (norm DO-178B, level A). Certification reduces the development costs as some validation/test/verification can be done directly to the source code instead of the target code. This is nonetheless not a formal certification. Instead, certification is on the development process and traceability between the source code and the target code. The objective is maintenability in the long term (typically 30 to 40 years for avionic).

• translation validation


• flow representation


• certified compilation


• lar code


• compilation run


• validation tool


• between every


• code


• using model-checking tool

Sujets

• Siegel
• Tristán

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 17
• Langue: English

Extrait

Formal translation validation between synchronous data-flow equations and application to a Lustre compiler

Master 2 Internship

November2011

Level :M2R Length :6 months (spring 2012) Advisor :Marc Pouzet ([e-mail]) ´ Location :raP0si5r,4d’uem,Ul2375De´nfortd’IemenpartoNelocE,euqitamreeuri´eupeSalrm cedex 05. Prerequisite :This internship is for a student with strong interest and skills in functional program- ming, the use of the Coq proof environment, the semantics and implementation of programming languages and reactive systems. Collaboration :The work can be continued with a PhD. thesis, in the PARKAS group, in colla- boration with the SCADE team of Esterel-Technologies.

Research Context

1 The synchronous data-flow language SCADEis used for implementing reactive systems in various critical domains such as nuclear energy, civil avionic, railways, etc. These uses have called for the “certification” of the C code generator of SCADE with the highest safety requirements (norm DO-178B, level A). Certification reduces the development costs as some validation/test/verification can be done directly to the source code instead of the target code. This is nonetheless not a formal certification. Instead, certification is on the development process and traceability between the source code and the target code. The objective is maintenability in the long term (typically 30 to 40 years for avionic). The certification of SCADE explains much of its success and is unique on the place. This certification is nonetheless extremely heavy and difficult to maintain while making the language and compiler continuously evolve. The problem we address here is the use of formal tools to increase the safety of the compiler, to simplify the certification process and to propose method that can be applied to an existing industrial compiler. 2 We have developed the compiler Velus, a prototype compiler that goes from Lustre to an imperative language and that use Coq as a development language. The compiler organisation is that of SCADE [1]. The different intermediate languages used in the compiler together with their

1.http://www.esterel-technologies.com 2. Velusstands for “Verified Lustre”.

1