Ce projet de recherche doctorale est publié a été réalisé par Dumitru POTOP-BUTUCARU

# Description d'un projet de recherche doctoral

### Formal certification of real-time implementations

**Mots clés : **

**Directeur de thèse** :
Dumitru POTOP-BUTUCARU

**Unité de recherche** :
INRIA-Paris

**Ecole doctorale** :
École Doctorale Informatique, Télécommunications, Électronique de Paris

**Domaine scientifique principal**: Divers

### Résumé du projet de recherche (Langue 1)

### Résumé du projet de recherche (Langue 2)

For example, the semantics of the application running in the presence of the underlying architecture can be analyzed to compute worst-case execution time (WCET) bounds. The real-time operating system, approximated by a scheduling mechanism and driven by additional real-time constraints, maps the application on the architecture,

introducing further timing overheads that must be taken into account.

The PhD student will start by formally modeling the application software (which has a coarser, task-level grain, as opposed to existing representations used in compiler certification) and the execution platform (hardware and basic software). We will consider execution platforms identified as representative by the Assume project (Kalray MPPA 256 and simple multi-cores on the hardware side, bare metal and ARINC 653-based on the software side).

Using the resulting models, the PhD student will then incrementally prove the compilation algorithms of Lopht. He/she will start with the real-time scheduling algorithm, with optimizations switched off. The PhD student will then consider various optimizations and also code generation algorithms such as the synthesis of communication

and synchronization. The work will combine program proof and translation validation techniques, using the Coq proof assistant for

specifications and proofs.

### Informations complémentaires (Langue 1)

### Informations complémentaires (Langue 2)

MSc degree in Computer Science or Computer Engineering, or equivalent. Good academic record. Previous exposure to formal modeling and/or verification techniques, concurrency theory, real-time systems, or compilation is considered a plus.

Location:

The successful candidate will join the AOSTE Research Group at INRIA Paris:

http://www.inria.fr/centre/paris-rocquencourt

http://www.inria.fr/en/teams/aoste

References:

[1] X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009.

[2] D. Potop-Butucaru, R. de Simone, Y. Sorel, and J.-P. Talpin: Clock- driven distributed real-time implementation

of endochronous synchronous specifications. In Proceedings EMSOFT’09, Grenoble, France.

[3] T. Carle. Efficient compilation of embedded control specifications with complex functional and non-functional

properties. PhD thesis. http://www.theses.fr/2014PA066392 .