Model-checking appliqué à un système d’agents mobiles

Vérification des systèmes temps-réel

Dans la littérature des algèbres de processus, il existe plusieurs approches de la vérification. L’une d’elles consiste à prendre deux descriptions d’un même système et de prouver leur équivalence sous certaines conditions. Généralement, une description est appelée la spécification et l’autre l’implémentation qui est souvent écrite en respectant des détails techniques supplémentaires. Cette preuve d’équivalence utilise une propriété souvent structurelle sur la spécification. Cette forme de vérification a ses limites, en particulier dans le cas de spécification partielle.

Cette approche s’intéresse à certains aspects du système et ignore totalement les autres. Une autre approche, plus adaptée dans notre cas, est basée sur l’emploi de logique modale ou temporelle. Ces logiques ne possèdent pas les mêmes structures sous-jacentes que les algèbres de processus, aussi, elles permettent d’écrire des spécifications ayant une autre forme d’abstraction. A partir de telles spécifications, il est alors possible d’évaluer une formule logique et de conclure si elle respecte ou pas le modèle exprimé en utilisant une algèbre de processus.

Les logiques utilisées ont souvent un faible pouvoir d’expression et il est même parfois difficile d’exprimer qu’un comportement est cyclique ou non. Des logiques plus intéressantes telles que le modal µ-calcul [AN01], associé à une algèbre comme le π-calcul, ont une définition basée sur des systèmes de transitions étiquetées.

Cela rend la construction de tels modèles plus facile à obtenir. D’autres logiques temporelles nous permettent d’utiliser des outils puissants tels que des ModelCheckers. Ainsi, un modèle à états finis est construit depuis une spécification afin de faire de la preuve. Il existe plusieurs formes de logiques temporelles avec des opérateurs pour exprimer des propriétés du type : « pour toutes les futures exécutions, il y a . . . »

Systèmes d’automates

Les systèmes qui se prêtent le mieux aux techniques de model-checking sont ceux facilement représentables par des automates (cf Définition 3.1). Ainsi, toute description à base de comportement à états tel que le processus W orker spécifié dans le chapitre 2 est un bon candidat à une telle transformation. Définition 3.1 (Automates) Un automate A est défini par le quintuplet hQ, E, T, q0, ℓi où : – Q est un ensemble fini d’états ; – E est l’ensemble fini des étiquettes des transitions ; – T ⊆ Q × E × Q est l’ensemble des transitions ; – q0 est l’état initial de l’automate – ℓ est l’application qui associe à tout état de Q l’ensemble fini des propriétés élémentaires vérifiées dans cet état.

La représentation du temps

Il n’est pas réaliste de considérer que la durée d’un traitement est fixe, le traitement pouvant se terminer plus tôt ou plus tard que prévu, sans compter les pannes possibles de machines ou encore les pertes de messages provoquant un ralentissement global du système. Deux méthodes de modélisation du temps s’opposent : le temps discret et le temps dense. Notons que dans cette thèse, nous considérons que le temps s’écoule de façon continue. La notion de 63 Chapitre 3. Model-checking appliqué à un système d’agents mobiles 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. Il existe cependant des travaux considérant une modélisation discrète du temps [Mag07]. La sémantique des modèles temporisés s’exprime en termes de systèmes de transitions temporisés (STT) où le domaine de temps, que nous notons T, peut être l’ensemble N des entiers naturels, l’ensemble Q≥0 des rationnels positifs ou nuls, ou l’ensemble R≥0 des réels positifs ou nuls.

Nous supposons par la suite que le domaine de temps T est l’ensemble R≥0. Nous donnons la définition formelle : Définition 3.2 (Système de transitions temporisé) Un système de transitions temporisé (STT) est un quadruplet T = (S, s0,→, Σ) où : – S est un ensemble d’états de contrôle ; – s0 est l’état de contrôle initial ; – → ⊆ S × (T ∪ Σ) × S est la relation de transition ; – Σ est un ensemble d’actions.