Modélisation à l'aide de machines à états

A. Construire un modèle

Systèmes réatifs: interaction avec l'environnement. L'environnement pourrait être un ensemble d'autres composantes ou des composantes externe au système, e.g. des usager.
Deux aspects de modélisation:
- La structure (souvent statique - ne changeant pas avec le temps): Un système consiste de composantes - et sous-composantes. Chaque composante a des interfaces (un ou plusieurs). A chaque interface, certains types d'interactions peuvent se réaliser (quelques fois, l'ensemble des interactions possibles est appelé l'alphabet de l'interface, ou de la composante). Des notations possibles sont:
  - dessins informels
  - structures en termes de blocs et sous-blocs, comme en SDL (voir structure du daemonGame en SDL; "composite structure" de la documentation TAU)
  - en UML: on utilise les diagrammes de classes et/ou le diagrammes de structure composite (voir modélisation avec UML)
- Le comportement dynamique: cela veut dire, dans quelle ordre et à quel moment les interactions vont se faire. Cet aspect est plus difficile à modéliser parce que les séquences d'interactions à considérer pourraient être arbitrairement longues, même infinies (par exemple, un téléphone marche toujours - au moins en modèle). Chaque sous-composante qui n'est pas decrite comme une composition de sous-sous-composantes doit être définie par un comportement dynamique en termes de sequences d'interactions possibles. Des notations possibles sont:
  - explications informelles
  - des diagrammes de séquencement UML (ou "Message Sequence Charts" (MSC))
  - des diagrammes d'activités UML
  - des machines à états. Il existent différentes versions de machines à états. Dans ce cours nous allons voir les versions suivantes:
    - Systèmes à transitions étiquettées (Labelled Transition Systems - LTS). Un LTS a un nombre fini d'états qui sont connectés par des transitions. Chaque transition a un étiquette qui représente l'interaction qui s'exécute quand la transition se fait. L'ensemble des étiquettes d'un LTS est appelé l'alphabet de l'LTS. Différents LTSs peuvent communiquer (c'est-à-dire, coordonnent les interactions) en partageant un sous-ensemble de leur alphabets. Les interactions partagées peuvent seulement être exécutées quand tous les LTS sont prèt à faire une transition qui est étiquettée par l'interaction en question. On appelle cela un rendezvous. Note: Les automates accepteur discutés dans le module 2 de ce cours sont en effet des LTSs à lesquels on a ajouté un sous-ensemble des états "acceptant".
    - Automates de Mealy, aussi appellés automates d'états finis (Finite State Machines - FSM). Comme un LTS, un FSM a un nombre fini d'états. Mais les interactions sont groupées en entrées et sorties. Chaque transition est normalement étiquettée par une interaction d'entrée et une interaction de sortie. Quand la machine est dans un état et une interaction d'entrée arrive pour laquelle il y a une transition de l'état courant, alors la machine fait cette transition dans un nouvel état et génère l'interaction de sortie marquée par la transition. La sortie d'un FSM devient normalement l'entrée d'un autre FSM ou une entrée à l'environnement. La transmission d'une sortie d'une machine vers une autre machine (pour laquelle l''interaction devient une entrée) implique normalement un certain délai et/ou mise en file d'attente. Note: Mealy a décrit de telle machines dans les années 1950 pour modéliser des circuits électroniques.
    - FSMs étendus (EFSM). Pour obtenir une puissance de modélisation plus élévée, on étend souvant les FSM en permettant des entrées et sorties avec des paramètres de types de données variés et en prévoyant des variables locales pour stocker des valeurs reliées aux paramètres des dernières interactions ou des résultats intermédiaires de calcul, souvent destinées pour définir les valeurs des paramètres des sorties. Les diagrammes d'états de UML (State diagrams) sont une notation particulière de EFSM. La version actuelle de UML supporte la notation orientée état (héritée de la version 1 de UML) et la notation orientée transition (hérité de SDL qui est maintenant un profile de UML). Dans ce cours, nous utilisons normalement le version SDL.
    - Autres types de machines d'état:
      - Machine de Moore: Comme des FSM, mais la sortie est continue, comme la valeur d'une variable (ou d'un circuit électronique), et cette sortie dépend seulement de l'état de la machine. Pour la conception de matériel, il est facile de composer plusieurs machines de Moore en prenant la sortie d'une machine comme entrée d'une autre; et on utilise une horloge globale pour déterminer les instants quand une machine lit son entrée et initie sa transition correspondante. On obtient un système syncrone.
      - Automates accepteur (AA): Ce sont des LTS pour lesquels, en plus, on a spécifié un sous-ensemble des états comme "acceptant". Ils sont utilisés pour définir des ensembles de séquences d'exécution. En contrast au LTS qui acceptent toutes les séquences qu'ils peuvent exécuter, un AA peut seulement accepter des séquences finies, en effet, celles qui amenent l'automate dans un état acceptant après la lecture du dernière entrée. Dans le module 2 de ce cours, on utilisera des AA pour définir des séquences de caractères ou de mots qui font partie d'un langage.
  - Exemple: Machine à café (la vue de l'usager: esquisse d'interface; structure: esquisse)
    - Modélisation des interactions: Considérons une interaction par bouton. Comment ça marche ? - Considérons un photocopieur: Il y a un bouton Go. Quand on le pousse deux fois, est-ce que l'on obtient deux copies ?
      - Modèle d'interactions syncrones (relativement abstrait): aussi appelé rendezvous (les deux parties doivent être dans un état prèt pour l'interaction). Comment l'état prèt est-il indiqué à l'usager de la machine ?
        
        Si l'on fait l'hypothèse que le temps d'exécution d'une interaction est très court, on peut considérer que, dans le modèle, il y a seulement une seule interaction à la fois dans tout le système. Ceci est appelé la sémantique à interlacement ("interleaving semantics"). Comment peut-on alors modéliser deux interactions simultanées ?
        
        Souvent on considère des interactions syncrones asymmétriques où une côté est toujour prète pour une interaction; par exemple dans le cas d'un appel de procédure dans les langages séquentiels.
      - Modèle d'interactions asyncrones: basé sur la transmission de messages; ceci est à un niveau plus bas que le rendezvous - on doit s'occuper des messages en transit, ce qui est complexe.
        
        Avec fiabililté (pas de pertes de messages): un message de sortie est stocké dans une file jusqu'à ce qu'il soit consommé comme entrée par la composante de destination. On a besoin de contrôle de flux (pour éviter que trop de messages s'accumulent dans la file avant d'être traités).
        
        Avec possibilité de perte de messages (comme la transmission de paquets IP dans l'Internet): si les messages s'accumulent trop, ils seront perdus; pas besoin de contrôle de flux, mais la perte de messages doit être prévue par les partenaires en communication.
        
        La situation où un message arrive et la composante receptrice est dans un état pour lequel il n'y a pas de transition de reception definie pour ce message, est appelée "reception non spécifiée". Elle indique normalement une erreur de conception.
    - Modèle LTS de la machine à café (esquisse informel - et notation utilisée par l'outil LTSA) - seulement la vue de l'usager est modélisée (exigences)
    - Modèle FSM de la machine à café (dans la notation supporté par l'outil Telelogic TAU ) - le modèle est plus détaillé: en plus de la vue de l'usager, il identifie deux composantes internes (le controlleur et le "hardware" qui produit les boissons), et la communication entre les deux composantes internes est aussi décrite.
  - Un autre example qui montre l'utilisé de la communication par rendezvous (formalisme utilisé par les LTSs):
  - Another example showing the usefulness of modeling with rendezvous communication (LTS formalism): Un modéle LTS d'une porte - et un modèle FSM
    - Dans cet exemple, l'interface entre la porte et l'usager de la porte est modélisé par une machine d'états. Ce type de modèle est appelé "modélisation de protocole" en UML (parce que les règles dynamique d'un interface d'un objet sont appelées "protocole" en UML) - en contrast avec la définition structural d'un interface en terme des méthodes et leurs paramètres. Il est important de noter que la modélisation d'un interface par une machine d'états fait du sense seulement s'il n'y a pas de collisions de messages; si les deux parties peuvent prendre des initiatives indépendantes, de telles collisions peuvent arriver, et il faut modéliser le protocole par deux machines d'états (une pour chaque côté - voir example de la machine à café) pour pouvoir comprendre ce qui peut arriver (comme expliqué par moi en 1977).

B. Vérifier des propriétés d'un modèle donné

Il y a deux types d'activités de V&V (vérification et validation):
- Validation: s'assurer que les propriétés du système satisfont les attentes des usagers et propriétaires
  - Ceci donne lieu à la "qualité du système" (terme utilisé dans le livre de Braek)
  - On se demande: " Est-ce que nous construisons le bon système ? "
  - Outils de support:
    - exécution simulée de la spécification fonctionnelle (e.g. en utilisant Telelogic TAU ou LTSA) et discussion avec les usagers et propriétaire concernant les traces d'exécution obtenues.
    - vérification de la consistance interne et contraintes générales du modèle: pas de problèmes de conception tel que blocages, réceptions non spécifiées (arrivée d'un message non attendu dans l'état courant), des boucles sans progrès, etc.
      - utiliser la fonctionalité ** de l'outil Telelogic TAU
      - utiliser la fonctionalité ** de l'outil LTSA
- Verification: s'assurer qu'un modèle plus détaillé (e.g. conception détaillée) satisfait les propriétés spécifiées par un modèle donné plus abstraite (e.g. document des exigences)
  - Ceci donne lieu à la "qualité du processus" (terme utilisé dans le livre de Braek)
  - On se demande: " Est-ce que nous construisons le système de la bonne manière ? "
  - Outils de support:
    - vérifier si une diagramme de séquencement donnée (correspondant à un cas d'utilisation) peut être réalisée par une machine d'états donnée (utiliser la fonctionalité ** de l'outil Telelogic TAU; avec l'outil LTSA, composer la séquence d'interactions donnée avec la spécification du modèle)
    - Vérification de modèles ("model checking"): vérifier que des propriétés données sont satisfaites par un modèle donné. On distingue des fois entre propriétés de "safeness" (est-ce que les événement qui arrivent sont valides ? - utiliser la fonctionalité ** de l'outil LTSA) et de "liveness" (ou progrès - utiliser la fonctionalité ** de l'outil LTSA)

C. Commentaires sur le non-déterminisme dans les modèles

Un modèle est non déterministe s'il admet plusieurs comportements. Un tel non-déterminisme est souvent introduit intensionellement, parce qu'à un niveau d'abstraction on voudrait laisser plusieurs options de comportement, ou il est claire que certains aspects du comportement ne peuvent être déterminés, par exemple, parce que les vitesses d'exécution de certains processus concurrents à l'intérieur du système ne sont pas connues. Voici quelques exemples:

Séquencement non déterminé par une diagramme de séquencement. Le diagramme (a) ci-dessous définit une seule séquence d'exécution des interactions, c'est envoyer a, recevoir a, envoyer c, recevoir c, envoyer b, recevoir b, envoyer d, recevoir d. Par contre, diagramme (b) permet plusieurs ordres différents pour l'exécution des primitives envoyer et recevoir; par exemple, l'ordre entre envoyer a et envoyer c n'est pas défini; similairement, l'ordre entre recevoir a et envoyer b n'est pas défini. On dit que le diagramme montre un ordre partiel, par exemple, le fait que recevoir b est avant envoyer d.

Non-déterminisme du à des vitesses d'exécution différentes: Les deux modèles FSM ci-dessous, quand ils sont exécutés conjointement en échangeant des messages entre eux, pourrait donner lieu à une séquence d'exécution qui correspond au diagramme de séquencement (b) ci-dessus. (Note: Une transitions étiquettée "!xx" représente une transition spontanée, seulement la sortie xx est indiquée; une transition étiquettée "?xx" est initiée par une entrée xx - elle n'a pas de sortie.) Par contre, si la vitesse de transmission du message c était plus rapide, ou la vitesse d'exécution de la machine A plus lente, le message c pourrait arriver quand la machine A est dans l'état 2. Ceci serait une reception non spécifiée (la reception de ce message n'est pas définie dans l'état actuel de la machine; ceci doit être considéré comme une erreur de conception). Nous concluons que la conception d'un système où les machines A et B communiquent comme considéré ici, est mauvaise..

Pour améliorer la conception des deux machines A et B, on est donc amené à additionner quelques transitions supplémentaires pour la reception de certains messages dans certains étaits. Voici une solution proposée (sans la transition en traits coupés):
Il est important de noter que les deux machines peuvent générer aussi des séquences de séquencement différentes du diagramme (b) ci-haut. Par exemple, lel message c pourrait arriver avant que le message b est envoyé par la machine A. Ceci est une observation générale: Souvent, un diagramme de séquencement donné implique d'autres diagrammes de séquencement, c'est-à-dire, ile est impossible de trouver deux machines qui réalisent le diagramme de séquencement donné sans aussi réaliser d'autres diagrammes de séquencement (les derniers sont appelés "implied scenarios" - séquencement impliqués).
Le point principal ici, c'est que deux machines, comme ci-dessus, peuvent donner lieu à un grand nombre de séquences d'exécution différents dépendant des vitesses relatives et des délais de transmission des messages. En pratique, cela veut dire que l'on ne peut pas prédire une séquencement particulière lors de l'exécution du système. Le système - même son implantation - est non déterministe. Ce non-déterminisme pourrait même donner lieu à des résultats fort différents: Si la transition avec entrée c dans l'état 2 de la machine à gauche est remplacée par la transition en traits coupés qui mène à l'état X et si le comportement de la machine dans l'état X est très différent (e.g. déclencher une explosion); alors la conception de ce système impliquerait qu'il y a la possibilité d'une explosion, mais cette explosion ne pourrait pas être prévu pour une exécution particulière (parce que l'on ne pourrait pas prévoir si le message c est reçu apès le message a et avant que message b soit envoyé).

Comportement non déterministe d'une machine à états
- Sorties non déterministes: Le diagramme FSM ci-dessous (à gauche) peut produire deux sorties différentes quand l'entrée a est fournie. Laquelle sera produite n'est pas spécifié. Cette spécification reflète un niveau d'abstraction du modèle où on ignore les paramètres de l'interaction a; en effet, dans un modèle plus détaillé on pourrait peut-être définir une condition, dépendant des paramètres de l'entrée et des valeurs de variables d'état, qui définit quelle sortie sera produite. Le modèle abstrait est non déterministe. Notes: (a) Dans certains cas, une implantation faisant un choix aléatoire pourrait être appropriée. (b) Le diagramme à droite montre le comportement de l'"usager" du modèle à gauche qui reste en synchronisation avec le modèle à gauche par ces interactions (c'est le comportement dual obtenu en échangeant entrées et sorties).
- Des LTS non déterministes: Les trois LTS ci-dessous représentent un "sender", un tampon ("buffer") et un "receiver". L'opération put entre des données dans le tampon et l'opération get permet au "receiver" de reçevoir les données dans le tampon. Le tampon a une interaction local (non couplée avec l'environnement) appellé loss qui représente la perte des données dans le tampon. Quand le "receiver" a reçu des données, il est prèt à faire une interaction (rendezvous) ack avec le "sender".
  - Le diagramme ci-dessous à gauche représente le comportement obtenu pour la composition du tampon avec le "receiver". Le nom d'état "1, 2", par exemple, veut dire que le tampon est dans l'état 1 et le "receiver" est dans l'état 2.
  - The left diagram below shows the behavior of the composition of the buffer with the receiver. The state name "1, 2", for instance, means that the buffer is in state 1 and the receiver is in state 2. Voici la composition (tampon avec "receiver"):
  - Si nous considérons la composition comme une boite noire, nous ne pourrions pas voir les interactions get et loss. Le diagramme au milieu montre cela en remplaçant les noms de ces interactions avec tau (ce qui veut dire une transition invisible, interne et spontanée). Ce LTS est dite non déterministe (non déterministe pour l'observation de son état - ou "state non-deterministic"), parce que, après avoir observé une certaine séquence d'interactions observables, on ne peut pas savoir dans quel état le LTS se trouve; par exemple, après la séquence <put, ack, put> on ne peut pas savoir dans quel état le modèle se trouve parce que les transitions internes ne sont pas observables. Conclusion: Un LTS contenant une transition spontanée est non déterministe.
  - On pourrait aussi considérer le LTS à droite. Il est équivalent au LTS au milieu - il définit les même séquences d'interactions visibles. Il n'a pas de transition spontanée, mais il est aussi non déterministe, parce qu'il y a deux transitions avec le même étiquette qui vont du même état dans deux états différents. Si cette interaction est observée, est la machine était dans l'état de départ des deux transitions, alors on ne sait pas dans quel état la machine sera après l'interaction en question.

Page créée: 22 janvier 2008; dernière mise à jour: 22 janvier 2010