Expliquer le fonctionnement d’un système en langage naturel
Modéliser formellement le système
Approche traditionnelle pour vérifier un système
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
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
Nous allons utiliser une méthode formelle appelée le Model-Checking
Vous avez vu dans cette UE par exemple :
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
Une logique temporelle décomposée en deux parties :
Cas particulier des réseau de Petri :
Generalized Mutual Exclusion Constraints (GMEC)
markingBounded(k)
vraie si toutes les places ont k
jetonsdeadlock
vraie si aucune transition franchissableM(P1) + 3 × M(P2) >= 3
(M(P3) and M(P4)) or M(P2)
markingBounded(1)
Représentation en arbre de
Pour un réseau de Petri : arbre des marquages
Forumle | Quantificateur | Qualificateur |
---|---|---|
AFφ | dans toutes les branches | il y a un état qui satisfait φ |
AGφ | tous les états satisfont φ | |
AXφ | le deuxième état satisfait φ | |
A[φ U ψ] | il y a un état qui satisfait ψ et tous les états avant satisfont φ |
Forumle | Quantificateur | Qualificateur |
---|---|---|
EFφ | il existe une branche | il y a un état qui satisfait φ |
EGφ | tous les états satisfont φ | |
EXφ | le deuxième état satisfait φ | |
E[φ U ψ] | il y a un état qui satisfait ψ et tous les états avant satisfont φ |
AF (M(P1) + 3 × M(P2) >= 3)
EF((M(P3) and M(P4)) or M(P2))
EX(markingBounded(1)
)
Formule φ = “J’aime le chocolat”
(nous n’utiliserons pas dans les TP et projets)
EF(AG) (there Exists a path / Finally / along All paths / Globally)
Nous allons utiliser le model-checker Roméo
Roméo utilie un CTL allégé :
Comment exprimer “la transition T n’est jamais franchissable” ?
La transition n'est pas franchissable si nous n'avons jamais ses places d'entrée qui contiennent en même temps un tokenAG(M(P1)==1 and M(P2)==1)
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
AG(not M(Perreur ) == 1) -> False
Attention on mélange système et vérification !
Il est possible de donner des priorités sur les transitions dans Roméo
La transition avec le plus grand chiffre sera franchie en premier