étude de réseaux de Thomas par validation de propriétés LTL pour Pseudomonas aeruginosa

Les systemes temps reel critiques doivent souvent repondre a des exigences temporelles de bout en bout, exprimees au niveau modele, mais qui ne sont pour la plupart veriees qu’au niveau de l’implantation. Cet article se focalise sur trois exigences : la latence d’une entree vers une sortie, la fraicheur d’une sortie relativement a une entree, et enn la reactivite du systeme vis-a-vis d’une entree. Nous montrons que, en utilisant une approche synchrone enrichie par des horloges temps reel pour la modelisation du systeme, il est possible de calculer ces proprietes automatiquement en faisant abstraction des choix d’implantation.