Introduction aux techniques de conception sûre des systèmes embarqués en utilisant les approches formelles, c’est-à-dire basées sur des modèles mathématiques, pour la description et la vérification des propriétés de tels systèmes.

• Contrôle continu en TP
• Un examen écrit final

Les systèmes embarqués sont des dispositifs constitués de matériels et de logiciels soumis à des contraintes à la fois fonctionnelles (par exemple, la correction des fonctions réalisées) et non fonctionnelles (par exemple, des échéances temporelles à ne pas dépasser, des niveaux de qualité de service à respecter) pour réaliser des traitements, et agir sur leur environnement. Des exemples de domaines où l’on rencontre de tels systèmes sont les télécommunications, le nucléaire, l’avionique ou le médical. Ces systèmes sont souvent critiques, notamment en ce qui concerne les trois derniers domaines cités précédemment, à cause d’enjeux humains et économiques importants en cas de défaillance.

Ce cours a pour but de sensibiliser les étudiants à la problématique de la conception sûre des systèmes embarqués critiques en introduisant les enjeux associés et deux approches importantes :

• La programmation synchrone dédiée aux logiciels embarqués de contrôle/commande dans des domaines comme l’avionique, l’automobile ou le nucléaire. Elle se base sur des langages ayant une sémantique mathématique et accompagnés d’outils adéquats pour garantir la correction des propriétés à la fois fonctionnelles et non fonctionnelles des systèmes. Cette approche sera illustrée à l’aide du langage Signal et de son environnement Polychrony (dont la version industrielle est commercialisée par Dassault Systèmes) ;
• L'approche de validation formelle par « model-checking », qui permet la vérification de propriétés fonctionnelles sur un modèle du système. Les différentes étapes (modélisation, expression des propriétés, graphe d'analyse et vérification) seront illustrées sur un exemple concret.

• Transparents de cours au format PDF
• Sujets d’exercices avec corrigés

• Programmation en langage C
• Notions (très) élémentaires en mathématiques : ensembles, relations, systèmes d’équations
• Modélisation en réseaux de Petri ou en automate (machines à états)
• Problématique du contexte des systèmes critiques et temps réel