Modèle formel d’un automate UPPAAL

Le temps dans un automate

Différents critères peuvent influencer la durée d’un traitement. Ainsi, des pannes sont possibles ou encore les pertes de messages. Elles provoquent un ralentissement global du système ou perturbent la terminaison du traitement en cours.
Afin de modéliser le temps, deux méthodes de modélisation s’opposent : le temps discret et le temps dense. La notion de temps dense s’oppose à la notion de temps discret dans lequel un grain minimal d’écoulement du temps est défini, c’est à dire que rien ne peut se passer dans une période de temps plus petite. Ce point de vue, bien que souvent très proche de la réalité et bien adapté à de nombreux cas, semble une hypothèse forte pour des systèmes distants ne partageant pas d’horloges au sens synchrone. Notons que dans cette thèse, nous considérons que le temps s’écoule de façon continue.

Les automates temporisés

Proposés par Alur et Dill [56], les automates temporisés étendent les automates finis classiques avec la notion de temps. La notion de temps est alors ajoutée au modèle classique sous la forme d’horloges qui évoluent de manière continue avec le temps. Ces horloges supportent l’application de prédicats qui peuvent être de deux types :
– les gardes donnent des contraintes sur les horloges à respecter pour pouvoir exécuter une transition d’action ;
– les invariants donnent des contraintes à respecter pour rester dans un état.
On note ( ) l’ensemble des contraintes d’horloges sur , c’est à dire l’ensemble des combinaisons booléennes de contraintes atomiques de la forme ~ où x est une horloge ∊ , une constante ∊ ℕ et ~ un opérateur de comparaison (~ ∊ {=,<,>, ≤, ≥})
Formellement, un automate temporisé est défini comme suit :
Définition 3.3 : Automate temporisé
Un automate temporisé est un 6-uplet = ( , , 0, , , ∑) où :
• est un ensemble fini d’états de contrôle ou localités;
• est un ensemble fini d’horloges;

Logique temporelle

Une logique temporelle sert à énoncer des propriétés portant sur les exécutions d’un système. Ces propriétés font intervenir la notion d’ordonnancement dans le temps, comme par exemple : « une porte s’ouvre après avoir à appuyer sur l’interrupteur » ou une orchestration est invocable après le traitement de l’activateur.

La logique temporelle CTL

La logique CTL (pour Computation Tree Logic) a été définie au milieu des années 1980 [57]. Elle est interprétée sur des structures de Kripke, c’est à dire des automates finis dont les états sont étiquetés par des propositions atomiques. Elle permet d’exprimer des propriétés sur ces états.
Définition 3.6 : Syntaxe de CTL
Les formules de CTL sont décrites par la grammaire suivante où sont des propositions atomiques (phrases simples dont on peut déterminer dans un contexte si elles sont vraies ou fausses.) qui parlent des états. Elles donnent pour un état donné une valeur de vérité bien définie.
En CTL, chaque occurrence d’un combinateur temporel ( , , ou ) doit être immédiatement sous la portée d’un quantificateur de chemin ( ou ).
Ainsi, par exemple, signifie qu’il existe un chemin partant de l’état courant, et tel que sera vraie dans un état futur, et que tous les états intermédiaires vérifieront . De son coté, signifie que le long de tout chemin partant de l’état courant, le successeur de l’état courant satisfait . En d’autres termes, cela signifie que tous les successeurs de l’état courant satisfont .
signifie qu’il existe un chemin le long duquel est vérifiée à une certaine position et donc qu’il est possible d’arriver à un état vérifiant . signifie que est vraie à une certaine position le long de tout chemin, c’est à dire que est inévitable. indique que est toujours vraie pour tout état accessible. Enfin, signifie qu’il existe un chemin le long duquel est toujours vraie.
Les combinateurs booléens permettent généralement de relier plusieurs sous-formules grâce à la négation ¬, à la conjonction ∧ « et », à la disjonction ∨ « ou » et à l’implication logique⇒.

Temporisation de CTL

La description d’un système sous la forme d’un réseau d’automates temporisés permet d’énoncer des propriétés avec la logique CTL sur ce système. Ces propriétés sont alors uniquement temporelles et ne mettent pas en jeu les informations quantitatives fournies par les horloges. La possibilité de pouvoir énoncer des propriétés temps-réel devient nécessaire. Pour cela, nous utilisons une logique temporisée qui est une extension d’une logique temporelle par des primitives permettant d’exprimer des conditions sur les durées et les dates. La logique TCTL [58], version temporisée de CTL, fournit ce langage logique pour spécifier des propriétés temporisées adaptées aux systèmes temps-réels.
Définition 3.6 : Syntaxe de TCTL
Les formules de TCTL sont décrites par la grammaire suivante :
, ∶∶= 1| 2| ··· |¬ | ∧ | ∨ | ⇒ |
(~ ) | (~ ) | (~ ) | (~ ) | (~ ) | (~ ) | (~ ) | (~ )
Avec ∊ ℕ et ~ un opérateur de comparaison tel que (~ ∊ {=,<, >, ≤, ≥})
Il existe différentes familles de propriétés [59]:
• Les propriétés d’atteignabilité. Ce type de propriété permet d’énoncer qu’une certaine situation peut être atteinte. Généralement il est surtout intéressant d’utiliser la négation d’une telle propriété. Pour exprimer ce type de propriété en logique temporelle on utilise le combinateur en écrivant , ce qui signifie « il existe un chemin partant de l’état courant et sur lequel se trouve un état vérifiant ».
• Les propriétés de sûreté. Dans ce type de propriété, on cherche à énoncer que, sous certaines conditions, quelque chose ne se produira jamais. Dans des cas simples, ces propriétés peuvent être vues comme la négation des propriétés d’atteignabilité. Le combinateur exprime ce type de propriétés en logique temporelle.
• Les propriétés de vivacité. Par ce type de propriétés on énonce que, sous certaines conditions, quelque chose finira par avoir lieu. Ces propriétés sont plus « exigeantes » que les propriétés d’atteignabilité. Ces propriétés paraissent peu utiles car elles n’apportent aucune information : elles sont bien trop abstraites. Les systèmes temporisés apportent la notion de propriété de vivacité bornée qui énonce un délai maximal avant que la « situation souhaitée » ne finisse par avoir lieu.
• Les propriétés d’équité. Ce type de propriété se rapproche beaucoup du type énoncé pour les propriétés de vivacité. Nous énonçons, dans le cas présent, que sous certaines conditions quelque chose aura lieu (ou pas) une infinité de fois. Le terme « équité » signifie une répartition équitable. Nous pouvons signaler une propriété particulière, l’absence de blocage, qui énonce que le système ne se trouve jamais dans une situation où il est impossible de progresser. En logique temporelle, l’absence de blocage s’écrit , ce qui signifie « quel que soit l’état atteint, il existera un état successeur immédiat ».

Présentation de l’outil de model-checking UPPAAL

Les algorithmes de model-checking sont implémentés par des logiciels. Une importante activité de recherche concerne ces outils qui visent à augmenter leur efficacité et à repousser leurs limites. Il existe plusieurs model-checkers temporisés : UPPAAL et Kronos [60] par exemple. L’outil HYTECH [61] développé à l’université de Berkeley par Thomas A. Henziger et Pei-Hsin, Ho vise à vérifier des réseaux d’automates hybrides très généraux. Kronos, quant à lui, vérifie des automates à l’aide de propriétés exprimées à l’aide de TCTL. D’autres outils de vérification tels que l’outil SNAKE [62] permettent de générer l’espace d’états d’un modèle exprimé par un réseau de Petri. Nous ne nous intéressons pas spécialement à ce type d’approche malgré l’intérêt qu’ils représentent.
L’outil UPPAAL se démarque des deux autres outils par son interface graphique très conviviale. Son module de simulation est très performant et permet, lors de la phase de modélisation, de faire des tests du modèle pour détecter d’éventuelles erreurs dans la modélisation. UPPAAL est un outil de model checking pour les systèmes temps réels. Il est développé conjointement par les universités d’Uppsala et d’Aalborg et c’est en 1995 que la première version fut disponible [63]. Depuis, l’outil est en perpétuelle évolution grâce à un développement constant comme le montre l’étude de K. Larsen [64] et les nombreuses études de cas qui ont été réalisées, comme [65] [66] [67]. Tout cela atteste de la maturité et de la qualité de cet outil.