UMLEmb
UML
for
Embedded
Systems

Modélisation et vérification des systèmes embarqués

Enseignement à distance par Webex

Ce cours du mastère spécialisé systèmes embarqué est donné à distance par votre enseignant. Vous devez donc venir avec un casque et un micro.

Votre première tache est de vous connecter à la sesion framatalk. Pour cela, cliquer sur le lien ci-dessous. framatalk fonctionne dans tous la plupart des navigateurs. Pensez à autoriser votre navigateur à accéder à votre micro et haut parleur lorsque il le demande. Pensez aussi à couper votre micro lorsque vous ne parlez pas. Enfin, votre enseignant est disponible à tout moment pour répondre à vos questions.

Première partie

Cette première partie est consacrée à la découverte de la modélisation et de la simulation d'un système embarqué. Suivez bien les étapes suivantes, et n'hésitez pas à poser des questions à votre enseignant, soit par tchat, soit par visio.
Pour commencer, vous allez regarder une capsule vidéo qui explique les principes de la modélisation avec le langage UML/SysML.

Principes de modélisation



Modélisation avec TTool

Maintenant que vous connaissez les grands principes de la modélisation avec UML/SysML, nous allons utiliser un outil libre et à sources disponibles qui permet de réaliser des modélisation avec le profil UML appelé AVATAR. Pour correctement suivre cette vidéo, vous devez avoir TTool installé sur votre ordinateur.
  • TTool est installé sur les machines de la salle où vous êtes. Pour configurer TTool, démarrez un terminal, puis lancez la commande suivante:
  • $ /comelec/softs/opt/TTool/ttool/local_install/makeLocalInstall
    
    Pour lancer TTool, il faut suffit alors de faire, depuis le même terminal:
    ~/TTool_local/bin/ttool.exe
    
    ou :
    $ cd ~/TTool_local/bin
    $ ttool.exe
    



  • Si vous préfèrez utiliser votre ordinateur personnel, je vous suggère d'utiliser une version pré-installée de TTool disponible pour Windows/MacOS/Linux. Une fois l'archive téléchargée, décompressez là, allez dans le répertoire TTool, et démarrez TTool avec ttool.bat (Windows ... si cela ne fonctionne pas : allez dans ) ou ttool.exe (MacOS, Linux).


Une fois TTool installé, pour apprendre à modéliser avec TTool, regardez tout d'abord la capsule vidéo suivante (en anglais, n'hésitez pas à activer les sous-titres).

Un premier modèle avec TTool

Maintenant, nous allons mettre en application ces principes de modélisation sur un petit exemple : un contrôleur de pression.

Ce contrôleur de pression utilise un capteur de pression pour vérifier que la pression d'une cabine ne dépasse pas un certain seuil. Si ce seuil ("threshold" en anglais) est atteint ou dépassé pendant au moins deux lectures consécutives, alors ce contrôleur de pression doit démarrer une alarme pendant 60 secondes, puis l'arrêter uniquement si la pression est repassée en dessous du seuil.

Nous allons à présent ouvrir le modèle de conception du logiciel de ce contrôleur de pression. Pour cela, lancez TTool, puis faites :
  1. Accès au modèle. Menu "File", puis "Open project from TTool repository"

  2. Chargement du modèle sous TTool. Sélectionnez le "contrôleur de pression" (PressureController) et chargez le sous TTool, puis cliquez sur l'onglet "Design"

  3. Compréhension du modèle. Regardez les différents blocks du système. Le block "PressureController" et ses sous-blocks correspondent au logiciel modélisé. Les blocks "PressureSensor" et "AlarmActuator" correspondent à une modélisation de l'environnement afin de pouvoir simuler le système. Essayez aussi de comprendre les différentes machines à état de ce contrôleur de pression. Votre enseignant est bien entendu disponible pour répondre à vos questions.

  4. Simulation du modèle Simulez le modèle, tout d'abord aléatoirement, puis essayez d'obtenir les traces de simulation suivantes:
    • Le déclenchement d'une alarme
    • Le déclenchement d'une alarme, et l'observation de la réaction du système lorsqu'une haute pression est détectée alors qu'une l'alarme est déclenchée.
    • Le déclenchement d'une alarme puis l'arrêt de cette alarme
    • L'obtention d'une longue trace dans laquelle l'alarme ne se déclenche jamais.



Deuxième partie

Vérification de modèles

Si la simulation consiste à explorer quelques traces d'exécution du système, la vérification formelle de modèle a plutôt comme objectif d'analyser de façon exhaustive les traces possibles d'un système.

Principes de la vérification formelle d'un modèle AVATAR


En résumé, plusieurs techniques peuvent être utilisées pour effectuer des vérifications formelles :
  1. Utiliser l'accessibilité d'un état (en faisant un click droit dessus, puis "Reachability/Liveness"), puis lancer, via TTool, soit UPPAAL, soit le mode-checker interne.

  2. Utiliser des pragmas puis lancer UPPAAL via TTool.

  3. Générer un graphe d'accessibilité puis l'étudier (visualisation, minimisation).
Vous allez maintenant pratiquer ces différents moyens.

Vérification du contrôleur de pression

Ce document présente contient quelques transparents sur la vérification de propriétés avec TTool appliqué au contrôleur de pression. Certaines questions ci-dessous font référence à ce document.
  1. Prouvez que tous les états des machines à états sont accessibles

  2. Expliquez un à un les différents "safety pragmas" qui sont déjà présents dans le modèle. Avant de vérifier ces pragmas avec UPPAAL, dites si vous pensez qu'ils sont vrais ou faux. Vérifiez ensuite les pragmas avec UPPAAL depuis TTool.

  3. Générez le graphe d'accessibilité du contrôleur de pression. Minimisez le graphe en sélectionnant 4 actions de votre choix, et visualisez le résultat. Ce résultat-il celui attendu ?

Modélisation et vérification d'un autre exemple

A présent, vous allez travailler sur un autre modèle issu d'une spécification industrielle fournie par Airbus.

Le système à modéliser est celui d'un protocole de communication entre une tour de contrôle et un avion appelé "FANS". Le modèle à utiliser est fourni sous la forme d'un fichier xml à sauvegarder puis à ouvrir avec TTool.

Comprenez d'abord le modèle, puis effectuez les améliorations demandées :
  • Comprenez le modèle fourni en le lisant, en le simulant, etc.

  • Prenez en compte les pertes de message. Nous considérons à présent que le message FN_ACK peut être perdu. Lorsque l'avion (enfin, le ssytème embarque de l'avion) ne reçoit pas ce message après un certain temps, il effectue une retransmission jusqu'à obtenir le message FN_ACK. Modifiez votre modèle, et prouvez que le système finit toujours par envoyer un FN_ACK avant de terminer.

  • Nous considérons à présent que l'avion transmet au maximum 3 fois le messages FN_CON. Modifiez vos diagrammes. En particulier, ajoutez un signal envoyé au pilote lorsque les trois envois n'ont pas été suivis par un FN_ACK. Simulez votre système, et prouvez que le système finit toujours par terminer l'initialisation ou par envoyer un message d'erreur au pilote. Pour cela, l'on vous demande d'utiliser un safety pragma.


Pour aller plus loin

Supports de cours

Autres documents