UE Embedded systems: from high-confidence design to safe execution

Diplômes intégrant cet élément pédagogique :

Descriptif

This course is dedicated to the high-confidence design of critical applications, in the world of embedded systems. For safety-critical or even mission-critical systems, rigorous design methods are mandatory, from initial modeling to final verification. Transport, space, medicine and energy are example of domains using critical applications, where any unexpected execution could endangered human lifes. They may have to meet the requirements of standards such as DO-178 (aerospace), ISO 26262 (automotive), IEC 60880 (nuclear energy). Designers face diverse challenges, in particular due to the presence of concurrent components and the close interaction between software and hardware. The correctness of the application must be guaranteed, but also often non-functional properties related to performance, safety, security. A variety of methods have been developed for this purpose.

In this course we study on the one hand the principles of code generation from a formalized model of the application, and on the other hand solutions for the verification of properties, on the embedded software or on the system as a whole. Lectures are supplemented by practical work sessions and projects. More precisely, the first part is illustrated on code generation from the synchronous language Scade/Lustre. Based on the main principles of this industrial design language, it addresses the main questions related to how to preserve the semantic and timing properties during the code generation and implementation phases. From sequential code generation, to multi-core implementation, it focuses on the way to implement such a critical applications -- with issues regarding real-time multitasking, interference analysis, scheduling and mapping. The second part is devoted to verification of properties and code monitoring. It addresses verification of correctness or safety properties for hardware/software platforms, input/output conformance testing, software monitoring and verification at runtime. Applications range from astronomical image processing to decision algorithms for self-driving cars.

Be able to specify the expected behaviour of an embedded application, generate operational code with functional and timing guarantees, verify fundamental functional and non-functional properties.

Pré-requis recommandés

  • Fluency in programming in C, C++, Java
  • Good knowledge of first-order logic
  • Basics of multi-core architectures, multi-tasking applications, message passing and shared memory models of communication.

Informations complémentaires

Langue(s) : Anglais