Systèmes d'intervalles de correction formels

Cette séance de cours de l'instructeur se concentre sur la conception de systèmes intermittents formellement corrects, répondant aux défis d'assurer l'exactitude dans les systèmes sans batterie alimentés de façon intermittente. La séance de cours porte sur l'absence de définitions de l'exactitude dans les systèmes existants, les obstacles aux garanties d'exactitude et la stratégie de recherche utilisée pour identifier les conditions fondamentales d'exactitude. Elle s'inscrit dans l'aperçu formel du modèle, l'importance de la cohérence de la mémoire et la nécessité d'appliquer les contraintes simplement sans raisonnement concret en temps. La séance de cours traite également des implications des hypothèses non vérifiées dans les systèmes actuels, de l'élaboration d'une approche de type pour l'intermittence sécuritaire et de l'importance de la sécurité et du raisonnement complet pour les dispositifs de bord extrême.