Dans cet article, je vous propose de revenir sur la problématique de modélisation des systèmes concurrents et communicants. Ayant traité le sujet des systèmes à événement discrets [1] dans un article précédent, nous avions vu qu’il était possible de modéliser ces systèmes à l’aide de systèmes à transitions.
En effet, la modélisation des composantes communicantes et concurrentes peut se traiter par une modélisation a base de multiple Sed [2]en utilisant des architectures spécifiques comme celle de la théorie du contrôle par supervision de Ramadge et Wonham [3].
Ces approches sont intéressantes car elles permettent l'élaboration d’une solution en ligne du principe de contrôle commande. C’est a dire que le modèle du système va être supervisé par un modèle de contrôleur produit a partir d’une spécification des comportement autorisé. Le résultat est un ensemble d’interactions orientées selon le champs des possibles des comportements tolérés et ce, au fil de l'exécution.
Cette approche est typiquement une approche classique du contrôle commande et de l’automatique (un article dédié a l’approche générale du contrôle des systèmes en automatique sera réalisé prochainement) cependant elle comporte des limites et reste complexe à mettre en oeuvre. Surtout lorsque le système est en fait la composition des comportements d’un ensemble de sous systèmes eux même en interaction entre eux. Dans ce genre de situation, la complexité est lié a la combinatoire des comportements possibles et la modélisation de cette combinatoire est hautement sujette à l’erreur surtout si l’on cherche un modèle unique.
Face à ces problématiques, Il est alors important d'élaborer des stratégies afin de prendre en compte cette complexité avant la phase de mise en production et ces stratégies se trouvent dans le model-checking.
Ainsi le model checking [4] a pour intérêt de permettre l’analyse d’un système et de ses comportements selon ses différentes composantes locales et/ou globale en amont de sa mise en production selon différents critères afin de garantir l’absence de dead lock (etat dans lequel le système ne peut plus évoluer et revenir dans son état initial) ou de live lock (état dans lequel le système peut encore évoluer mais ne peut plus revenir dans son état initial). Ceci n’est pas le seul intérêt du model checking car il permet également de caractériser des propriétés dans un système et de valider des comportements souhaités.
Cette approche est pratique car elle n’a pas pour but de contraindre le système qui est alors toujours libre de fonctionner selon tous ses degrés de libertés mais juste de s’assurer que celui ci est la solution a notre besoin auquel cas alors il sera toujours possible d'élaborer une loi de commande qui elle même pourra aussi être validée par une phase de model checking.
Prenons le temps de détailler tout cela au travers d’un exemple.
Exemple
Considérons donc un robot avec quatre pattes. Chacune des pattes est l’association de deux moteurs pas à pas. L’un a la base de la patte permet d’avancer ou reculer celle ci et un autre a l’articulation permettant de lever la patte ou la reposer. C’est très simpliste mais cela permet quelques mouvements qui peuvent déjà devenir très complexe.La combinaison de ces deux mouvement permettant alors de réaliser des mouvement de plus haut niveau tels que la protraction (1) qui consiste a lever la patte et l'amener vers un point en avant en suivant une trajectoire curviligne et la rétraction (2) qui consiste a ramener la patte dans sa position initiale en suivant une droite
Nous utiliserons l’outil de model-checking LTSA [5] (qui s’appuie sur la notation FSP, Finite state Process [6]) pour effectuer la modélisation de notre système et effectuer le model checking
En FSP, la modélisation du comportement d’une pattes est donc l’association d’un moteur haut bas et d’un moteur avant arrière:
MoteurHB=(lever -> poser -> MoteurHB).
MoteurAR=(avancer -> reculer -> MoteurAR).
|| PATTE =(MoteurHB || MoteurAR).
A partir de ce système nous pouvons imaginer l’ensemble des comportements possibles de notre robot en déclinant ce modèle de patte en 4 exemplaires.
||PATTES = ({p1,p2,p3,p4}:PATTE).Représenter ce modèle n'aurait pas beaucoup d'intérêt car déjà trop gros pour être seulement pertinent mais pour se rendre compte, ce modèle possède déjà 256 états et 512 transitions.
Nous sommes face à une complexité de type exponentielle O^n
Moteurs
|
1
|
2
|
4
|
6
|
8 (4 pattes)
|
Nombre Etats
|
2
|
2^2=4
|
2^4=32
|
2^6=64
|
2^8=256
|
Nombre Transitions
|
4
|
2*2^2=8
|
2*2^4=64
|
2*2^6=128
|
2*2^8=512
|
Il faut noter que cet ensemble de comportement n’est pas celui attendu, il est beaucoup plus grand que nécessaire car pour chaque patte, il existe des comportement ne respectant pas les règles de protraction et de retraction. On définit une propriété de marche pour les mettre en évidence.
property MARCHEG = ({p1.lever,p3.lever} -> {p1.avancer,p3.avancer} -> {p1.poser,p3.poser} -> {p1.reculer,p3.reculer} -> MARCHEG).
property MARCHED = ({p2.lever,p4.lever} -> {p2.avancer,p4.avancer} -> {p2.poser,p4.poser} -> {p2.reculer,p4.reculer} -> MARCHED).
|| TEST=(PATTES || MARCHEG).
Compiled: MoteurHB
Compiled: MoteurAR
Compiled: MARCHEG
Composition:
TEST = PATTES.p1:PATTE.MoteurHB || PATTES.p1:PATTE.MoteurAR || PATTES.p2:PATTE.MoteurHB || PATTES.p2:PATTE.MoteurAR || PATTES.p3:PATTE.MoteurHB || PATTES.p3:PATTE.MoteurAR || PATTES.p4:PATTE.MoteurHB || PATTES.p4:PATTE.MoteurAR || MARCHEG
State Space:
2 * 2 * 2 * 2 * 2 * 2 * 2 * 2 * 15 = 2 ** 12
Composing...
property MARCHEG violation.
-- States: 176 Transitions: 1408 Memory used: 48580K
Composed in 48ms
|| TEST2=(PATTES || MARCHED).
Compiled: MoteurHB
Compiled: MoteurAR
Compiled: MARCHED
Composition:
TEST2 = PATTES.p1:PATTE.MoteurHB || PATTES.p1:PATTE.MoteurAR || PATTES.p2:PATTE.MoteurHB || PATTES.p2:PATTE.MoteurAR || PATTES.p3:PATTE.MoteurHB || PATTES.p3:PATTE.MoteurAR || PATTES.p4:PATTE.MoteurHB || PATTES.p4:PATTE.MoteurAR || MARCHED
State Space:
2 * 2 * 2 * 2 * 2 * 2 * 2 * 2 * 15 = 2 ** 12
Composing...
property MARCHED violation.
-- States: 176 Transitions: 1408 Memory used: 47479K
Composed in 16ms
On voit ici que le logiciel nous dit que les comportements de nos pattes peuvent ne pas respecter ces règles de marches et avoir des comportements autres.
On donc les utiliser comme contrôleur et les coupler avec les pattes du robot:
CONTROLLEUR_MARCHEG = ({p1.lever,p3.lever} -> {p1.avancer,p3.avancer} -> {p1.poser,p3.poser} -> {p1.reculer,p3.reculer} -> CONTROLLEUR_MARCHEG).
CONTROLLEUR_MARCHED = ({p2.lever,p4.lever} -> {p2.avancer,p4.avancer} -> {p2.poser,p4.poser} -> {p2.reculer,p4.reculer} -> CONTROLLEUR_MARCHED).
||SYSTEM=(PATTES || CONTROLLEUR_MARCHEG || CONTROLLEUR_MARCHED).Notre nouveau système que l’on peut schématiser comme suit:
Sur celui ci on va pouvoir vérifier maintenant nos précédents propriétés:
|| TEST3=(SYSTEM || MARCHEG).
Compiled: MoteurHB
Compiled: MoteurAR
Compiled: CONTROLLEUR_MARCHEG
Compiled: CONTROLLEUR_MARCHED
Compiled: MARCHEG
Composition:
TEST3 = SYSTEM.PATTES.p1:PATTE.MoteurHB || SYSTEM.PATTES.p1:PATTE.MoteurAR || SYSTEM.PATTES.p2:PATTE.MoteurHB || SYSTEM.PATTES.p2:PATTE.MoteurAR || SYSTEM.PATTES.p3:PATTE.MoteurHB || SYSTEM.PATTES.p3:PATTE.MoteurAR || SYSTEM.PATTES.p4:PATTE.MoteurHB || SYSTEM.PATTES.p4:PATTE.MoteurAR || SYSTEM.CONTROLLEUR_MARCHEG || SYSTEM.CONTROLLEUR_MARCHED || MARCHEG
State Space:
2 * 2 * 2 * 2 * 2 * 2 * 2 * 2 * 15 * 15 * 15 = 2 ** 20
Composing...
-- States: 121 Transitions: 308 Memory used: 37000K
Composed in 61ms
|| TEST4=(SYSTEM || MARCHED).
Compiled: MoteurHB
Compiled: MoteurAR
Compiled: CONTROLLEUR_MARCHEG
Compiled: CONTROLLEUR_MARCHED
Compiled: MARCHED
Composition:
TEST4 = SYSTEM.PATTES.p1:PATTE.MoteurHB || SYSTEM.PATTES.p1:PATTE.MoteurAR || SYSTEM.PATTES.p2:PATTE.MoteurHB || SYSTEM.PATTES.p2:PATTE.MoteurAR || SYSTEM.PATTES.p3:PATTE.MoteurHB || SYSTEM.PATTES.p3:PATTE.MoteurAR || SYSTEM.PATTES.p4:PATTE.MoteurHB || SYSTEM.PATTES.p4:PATTE.MoteurAR || SYSTEM.CONTROLLEUR_MARCHEG || SYSTEM.CONTROLLEUR_MARCHED || MARCHED
State Space:
2 * 2 * 2 * 2 * 2 * 2 * 2 * 2 * 15 * 15 * 15 = 2 ** 20
Composing...
-- States: 121 Transitions: 308 Memory used: 36363K
Composed in 26msEt conclure que nous n’avons plus de violations.
Bien sur cet exemple est très simpliste mais par l’explosion combinatoire de comportement, on se rend vite compte qu’il est difficile d’estimer même visuellement sur des structures “simple” que celles ci ont les comportement attendu et n’ont pas de comportements prohibés. A l’aide du model-checking, nous pouvons travailler de façon formelle sur le système en utilisant par exemple ici la notation FSP. A l’aide de la même notation, nous nous sommes restreint à la définition de propriétés très simple mais il reste possible d’aller plus loin en vérifiant des propriétés typique du model checking telles que
- est ce qu’une propriété arrivera un jour ?
- est ce qu’une propriété est invariante ?
- est ce qu’une propriété est récurrente ?
Cet article n'était qu’une introduction pour saisir les enjeux du model checking. Pour les prochains articles sur le sujet nous entrerons donc plus dans le détails des aspects formelles du model-checking.
Références
[1] http://un-est-tout-et-tout-est-un.blogspot.fr/2017/11/readysystemes-evenements-discrets.html[2] http://un-est-tout-et-tout-est-un.blogspot.fr/2017/11/finite-state-machine.html
[3] http://un-est-tout-et-tout-est-un.blogspot.fr/2017/12/supervisory-control-theory.html
[4] https://ti.arc.nasa.gov/m/profile/dimitra/publications/thesis.pdf
[5] https://www.doc.ic.ac.uk/ltsa/
[6] https://www.doc.ic.ac.uk/~jnm/LTSdocumention/FSP-notation.html
[7] https://www.lri.fr/~paulin/Logique/html/cours004.html
[8] http://queinnec.perso.enseeiht.fr/Ens/ST/ltl.pdf
[9] http://queinnec.perso.enseeiht.fr/Ens/ST/ctl.pdf
[10] https://fr.wikipedia.org/wiki/CTL*
Aucun commentaire:
Enregistrer un commentaire