Description du module

Informations générales

• 2 séances de 3h45 avec
  • cours
  • tutoriel
  • mini-projet en séance
• Evaluation par mini-projet en séance
• Contact : helene.coullon@imt-atlantique.fr, bureau B220

Contenu de la séance 1

• Cours Model Checking partie 1/2
• Tutoriel sur Roméo 1/2
  • construire un réseau de Petri
  • simuler un réseau de Petri
  • vérifier une propriété
• Mini-projet (par groupes)
  • choix de votre système
  • spécification en langage naturel
  • spécification en réseau de Petri
  • premières propriétés et correction du système

Contenu de la séance 2

• Cours Model Checking partie 2/2
• Tutoriel sur Roméo 2/2
  • autres proriétés et sous-réseau observateur
  • réseau de Petri temporisé
• Mini-projet (par groupes)
  • toutes les propriétés de votre système (1h)
  • préparation de l’oral (1h)
  • oral (15 minutes par groupe, total 1h30)

Evaluation 1/2

Mini-projet : 5 groupes (trois de 4, deux de 5)

• CG1 Comprendre et analyser, synthétiser un problème et/ou une situation complexe
• CG4 Critiquer et décider
• CG14 S’engager
• CG9 Communiquer (oral en séance)

Evaluation 2/2

Attendues pour l’oral

1. présenter votre système en langage naturel
2. démonstration : modélisation dans Roméo
3. présenter vos propriétés
4. démonstration : vérification dans Roméo

Introduction

Modélisation

Expliquer le fonctionnement d’un système en langage naturel

• exemple : documentation
• avantages : facile à lire et comprendre par un humain
• désavantages : peu fiable et peut être compris de différentes façons

Modélisation

Modéliser formellement le système

• exemples : réseau de Petri, automates
• avantages : fiable et précis
• désavantages : difficile pour un humain

Test

Approche traditionnelle pour vérifier un système

• facile à mettre en oeuvre
• utile à différentes étapes de la conception

Limitation : Exhaustivité des tests est souvent impossible

“Tester des programmes peut être un moyen très efficace de révéler des bugs, mais est irrémédiablement inadapté pour en démontrer l’absence.” E.W. Dijkstra

Indéterminisme et test

Un système est indéterministe si une exécution depuis un état donné peut mener à plusieurs état différents

Exemples : hasard, éléments externes au système, ordre d’exécution

L’indéterminisme augmente la difficulté des tests

Méthodes formelles

• représentation et modélisation abstraite et formelle du système
• techniques de raisonnement mathématiques sur le modèle pour en vérifier des propriétés

Méthodes formelles

Nous allons utiliser une méthode formelle appelée un Model-Checker

Analogie en physique

• système : un pont
• proriété : resister à des vents violents
• tests : tests en soufflerie sur une maquette
• méthode formelle : modéliser le pont et le vent et étudier mathématiquement la propriété

Outils de modélisation

Vous avez vu dans cette UE par exemple :

• la simulation à événements discrets
• les réseaux de Petri

Vocabulaire propriétés

• safety : proriétés de sûreté
  • le système n’entre jamais dans un état non-sûr
• liveness : propriétés de vivacité
  • le système finira par atteindre un état désiré

Langages de propriétés

Il existe également différents langages pour exprimer les propriétés formelles

Pour le Model-Checker nous allons utiliser :

Computational Tree Logic (CTL) qui permet d’exprimer des propriétés formelles temporelles sur un réseau de Petri notamment

Séance 1

Logique temporelle

Une logique temporelle décomposée en deux parties :

• langage pour décrire les propriété du système à un instant donné
  • “la place P contient n jetons”
  • “aucune transition ne peut être franchie”
• ajout de modalités temporelles
  • “il est possible que …”
  • “il est certain que …”
  • “… toujours …”
  • “… à un moment …”

Propriétés du système

Cas particulier des réseau de Petri :

Generalized Mutual Exclusion Constraints (GMEC)

• le marquage M (nb jetons)
• identification des places et transitions par un nom
• innégalités (<, <=, >, >=, ==, !=)
• opérateurs Bouléens (and, or, not, =>)
• markingBounded(k) vraie si toutes les places ont k jetons
• deadlock vraie si aucune transition franchissable

Exemples de propriétés

M(P1) + 3 × M(P2) >= 3

(M(P3) and M(P4)) or M(P2)

markingBounded(1)

CTL

Représentation en arbre de

• l’état actuel du système (à la racine)
• et ses états futurs pour les noeuds enfants

Pour un réseau de Petri : arbre des marquages

Quantificateurs CTL 1/2

• A = along All paths
  • toutes les branches doivent satisfaire la formule

Quantificateurs CTL 2/2

• E = there Exists a path
  • il doit exister une branche (au moins) qui satisfait la formule

Qualificateurs CTL

• F = Finally
  • doit être satisfaite par au moins un état dans la branche
• G = Globally
  • doit être satisfaite par tous les états de la branche
• X = neXt
  • dans l’état suivant de la branche
• U = Until
  • la première formule doit être satisfaite par tous les états de la branche jusqu’à ce que la deuxième formule devienne vraie à un moment

Visuel des combinaisons

Liste propriétés temporelles 1/2

Liste propriétés temporelles 2/2

Exemples de propriétés complète

AF (M(P1) + 3 × M(P2) >= 3)

EF((M(P3) and M(P4)) or M(P2))

EX(markingBounded(1))

Exemple d’imbrication

EF(AG) (there Exists a path / Finally / along All paths / Globally)

Exemple de tous les jours

Formule φ = “J’aime le chocolat”

• AGφ: “J’aime le chocolat maintenant et pour toujours, quelque soit mon futur”
• EFφ: “Il est possible que j’aime un jour le chocolat”
• AF(EGφ): “Il est toujours possible (AF) que je vais me mettre à aimer soudainement le chocolat pour le reste de ma vie”
• EG(AFφ): “Il est possible (E) que dans un futur et pour le reste des temps (G) il y aura toujours un moment (AF) où j’aimerai le chocolat”

Visualisation des imbrications

Roméo

Nous allons utiliser le model-checker Roméo

Roméo utilie un CTL allégé :

• pas de EX, AX
• pas de formules imbriquées

Tutoriel Roméo 1/2

Séance 2

Propriétés sur les transitions ?

Comment exprimer “la transition T n’est jamais franchissable” ?

Propriétés sur les transitions ?

Comment exprimer “la transition T2 n’est jamais franchie avant T1” ?

Il faut créer un sous-réseau observateur pour vérifier que cela n’arrive jamais

Sous-réseau observateur

Sous-réseau observateur

AG(M(Perreur ) == 0)

Attention on mélange système et vérification !

Arc lecteur

• arc entrant (entre place et transition)
• les jetons ne sont pas consommés lors du franchissement de la transition

Arc inhibiteur

• arc entrant (entre une place et transition)
• la transition n’est pas franchie si la place contient des jetons

Arc réinitialisateur

• arc sortant (entre une transition et une place)
• lorsque la transition est franchie le nombre de jetons dans la place sortante passe à 0

Réseaux de Petri temporisés

• extension qui ajoute du temps réel
• pour chaque transition un intervalle de temps est indiqué
• chaque transition est équipée d’une horloge
• la transition n’est franchissable que lorsque l’horloge est dans l’intervalle

Rédeaux de Petri temporisés

• un RdP standard est équivalent à un RdP temporisé où tous les intervalles sont [0,∞[
• les conditions d’horloge empêchent certaines executions
  • élagage de certaines branches des futurs possibles

Tutoriel Roméo 2/2