Concevoir des systèmes d'intervalles officiellement corrects

Cette séance de cours de l'instructeur se concentre sur la conception de systèmes intermittents formellement corrects, explorant les défis et les solutions pour assurer l'exactitude, la fiabilité et la sécurité dans les plates-formes informatiques de pointe. La séance de cours aborde des sujets tels que la définition des conditions d'exactitude, l'application de la cohérence de la mémoire, la gestion des contraintes de temps et l'utilisation de systèmes de type pour l'exécution intermittente en toute sécurité. Différents outils et modèles formels sont discutés, y compris le Curriculum pour le raisonnement par type et l'Ocelot pour l'application d'intrants frais et cohérents. La séance de cours souligne l'importance de la co-conception HW/SW, des abstractions de langage et des considérations de sécurité dans la construction de systèmes intermittents robustes.