Résumé
Ce cours est consacré à trois compléments aux cours de l’année, puis à la réponse aux questions envoyées par courrier électronique pendant l’année, et enfin à la réponse à celles posées en salle. Le premier complément concerne la preuve de correction du synchroniseur de l’instruction parallèle d’Esterel, fondé sur un codage 2-adique et central pour la sémantique et l’implémentation du langage. La preuve est formalisée dans le système de vérification Why développé à Orsay, qui appelle lui-même les deux solveurs SMT CVC et Alt-Ergo (voir les cours et séminaire du 23 mars 2016). Le deuxième complément approfondit le formalisme CHAM de la machine chimique développé à la fin des années en 1989 avec Gérard Boudol pour formaliser le parallélisme asynchrone. Le troisième complément présente comme exercice de vérification en CADP celui d’un système de perçage qui sert souvent d’exemple pour la vérification formelle.
Les questions écrites sont les suivantes :
- Peut-on concevoir des systèmes grandement distribués et sûrs, ou aussi des systèmes « tolérants les fautes », sortes d’hybrides entre preuves et sûreté de fonctionnement ?
- Sur les protocoles : il y a de nombreuses initiatives pour de nouveaux standards. Comment faire pour y exploiter les avancées théoriques présentées dans le cours ?
- Sur les optimisations de circuits, peut-on capitaliser sur les opérations déjà effectuées, par exemple quand on retrouve des sous-expressions logiques vues ailleurs ? Peut-on enregistrer les optimisations déjà réalisées dans des formats adaptés ?
