Résumé
Les systèmes temporisés sont ceux pour lesquels les contraintes liées au temps physique sont essentielles pour la correction du fonctionnement : systèmes embarqués temps-réel, protocoles de communication dépendant directement du temps ou soumis à des contraintes de délai de transmission, etc. Un formalisme standard pour les décrire est celui des automates temporisés, dont les transitions peuvent être gouvernées par des variables appelées horloges. Ces variables avancent toutes au même rythme en fonction du temps, elles conditionnent les transitions, et on peut les remettre individuellement à zéro lors de transitions. En nous appuyant sur des exemples écrits à l’aide du système UPPAAL décrit ensuite dans le séminaire, nous présentons le formalisme et la façon d’exprimer les propriétés à vérifier. Nous décrivons ensuite les algorithmes permettant de décider efficacement les propriétés des automates temporisés. Ces algorithmes de nature géométrique étudient les contraintes mutuelles que l’automate impose aux horloges, soit de façon exacte soit par interprétation abstraite. Ils traduisent le problème de vérification initial en ensembles d’inégalités aux différences d’horloges, dont on peut décider la satisfiabilité avec des algorithmes rapides, également utilisés dans les systèmes SMT décrits dans le cours précédent.
