Pourquoi le model checking ?

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

Pour juste nous rendre compte pour un système à 2 pattes le modèle correspondant serait celui ci:


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 26ms

Et 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 ?

Pour répondre à ces questions, il faudra utiliser des logiques spécifiques comme LP [7], LTL[8], CTL [9] ou CTL* [10], des logiques permettant de spécifier plus précisément nos propriétés.

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*

Evolution Java 7

Nous voila donc arrivé a la version 7. Cette version, tout comme la version 5 amène ses bouleversements mais dans une optique de simplification. Voyons en quoi.

Globalement je me suis inspirer de l'article de JmDoudou donc si vous voulez des détails, n’hésitez pas a aller le consulter.

Donc dans les grandes lignes, l'idée de cette version de Java est de simplifier et comme souvent, pour simplifier, on change la syntaxe afin de rendre plus lisible le code sauf pour le premier point qui lui consiste a permettre l’écriture des types entiers en binaire. Bon en dehors d'un besoin très spécifique, comme de traiter un protocole très bas niveau... je ne m’entendrais pas sur ce point.

Autre point de réécriture, celui de permettre d'utiliser des anderscores dans les nombres afin de faire des groupes de chiffres et simplifier la lecture.

Exemple:

1 2 3 4 5

int value = 1_146_789; value = 4_3; value = 4___3; value = 0b1001110_10001011_01001101_01000101; float pi = 3.141_593f;

Comme je l'avais évoqué dans la partie sur les enum  le switch/case n’était pas capable de traiter autre chose que des types primitifs ou des enum. Maintenant ces derniers pourront traiter des String.

Exemple:

1 2 3 4 5 6 7

String s="toto"; switch(s) { case "toto" : toto();break; case "titi" : titi();break; default: defaut();break; }

Bon après honnêtement moi les switch/case j'aime pas ça et souvent on peut les éviter par une bonne hiérarchie de classe (et ça va de même avec les if/then/else imbriqué) mais on retraitera de ce genre de sujet.

L’opérateur <>. alors la, clairement, il s'agit de Ze Sucre Syntaxique. En fait il n'apporte que de la lisibilité et c'est franchement pas mal. Je m'explique, le problème est simple, on est partie dans la construction d'une hiérarchie de classe avec un beau pattern composite et op on se dit tiens utilisons des generiques! Dans le principe c'est pas une mauvaise idée, au contraire sauf que souvent on se retrouve a declarer des listes de truc, machin avec des listes de chouettes shumrtz.

Exemple:

1	Map<Integer, Map<String,List<Truc>>> maStructure=new HashMap<Integer, Map<String,List<Truc>>>();

Bon je dis pas j'ai un peu exageré le trait....  quoique.... Enfin et bien l'operateur diamant permet d'ecrire juste:

1	Map<Integer, Map<String,List<Truc>>> maStructure=new HashMap<>();

Et le compilateur fait le reste du travail de résolution des types s'il en est capable et ca marche aussi pour les retours de fonctions:

1 2 3

private static Map<Integer, Map<String,List<Truc>>> titi() { return new HashMap<>(); }

Gestion des ressources. Il s'agit de permettre au bloc try de gérer lui-même la fermeture d'une ressource au lieu de devoir le faire via le finally employé jusqu’à la version 6. On aura alors une écriture plus simple, plus lisible et plus fiable avec laquelle on pourra continuer a gérer les erreurs et exceptions éventuelles mais ou la fermeture des flux se fera automatiquement.

Exemple:

1 2 3 4 5 6 7 8

try (BufferedReader bufferedReader = new BufferedReader(new FileReader("monfichier.txt"))) { String ligne = null; while ((ligne = bufferedReader.readLine()) != null) { System.out.println(ligne); } } catch (IOException ioe) { ioe.printStackTrace(); }

Enfin pour ceux qui voudront créer leur propre flux compatible avec le bloc try, il faudra implémenter l'interface java.lang.AutoCloseable

La gestion des exceptions a également été revu en java 7, et c'est une bonne chose car cette nouvelle gestion permet une gestion plus concise des anomalies et de leur type leur de reemissions d'exceptions.

En effet, maintenant, un bloc catch peut être défini pour un groupe d'exception possible permettant de factoriser leur traitements et d’éviter la multiplication des blocs:

1 2 3 4 5 6 7 8 9 10 11 12 13

try{ //TODO }catch (Exception1 e1) { //TODOX } catch (Exception2 e2) { //TODOX } catch (Exception3 e3) { //TODOX } finally { //TODO }

devient si les blocs TODOX sont identiques

1 2 3 4 5 6

try{ //TODO }catch (Exception1 | Exception2 | Exception3 e) { //TODOX }finally { //TODO }

C'est mieux quand même!

Pour la reemissions d'exceptions c'est simple, si vous catcher une exception a l'aide d'un sur-type mais que vous devez la reemettre avec un throw, et bien sur la définition de la méthode (a la suite du mot clefs throws) vous pourrez toujours utiliser la définition de type de l'exception initiale et non de son sur-type, sauf.... si vous imbriquez deux blocs try/catch.... Dans l'absolu ça permet de garder l'information initiale malgré un filtrage "trop globale".

java.nio.Path en remplacement de java.io.File.... bon ca parle de soi-même, c'est pour accéder plus simplement aux chemins comme sait le faire Python.... et oui dans les autres langages on trouve des trucs bien, il faut savoir en tirer parti... et couplé aux classes Files, DirectoryStream, Filter and coe, on obtient toutes les infos pour traiter les fichiers et toutes leurs proprietés. Dommage que ca n'ai pas été fait déjà a la version 6 qui avait déjà tenté une mise a jour.... a oui pour info tout cela s’appelle l'API NIO 2 et en plus elle intègre la possibilité de traité des flux de façon asynchrone.

Sinon encore des updates dans awt/Swing .... je rentre dans le détail?

Ah si! un truc très sympas, l'ajout du package java.lang.invoke qui enrichi la réflexion deja existante avec des capacités de recherche de méthodes en respectant la visibilité. Cela fournira donc des objets, les MethodHandle, sortes de pointeur de fonction sur les méthodes ciblés. Il faudra faire un petit billet dédié a cette API associé a l'API réflexion. Ca sera très intéressant.

L'API de concurrence est peut être l'apport le plus significatif de Java pour cette version. Par contre son utilisation est loin d’être trivial car nécessitant de bien comprendre les conséquences de son utilisation. Ainsi cette API propose via la classe RecursiveTask de diviser le traitement de processus et les repartissant via des Thread dédiés sur les processeurs physiques de la machine. Ceci va permettre d'exploiter au mieux des ressources cependant attention une limitation en terme de synchronisation peu survenir ainsi une division trop élevé d'une tache en sous-tache pourra être contre productive car passant plus de temps a resynchroniser les résultats de Thread qu'a exécuter leur propre tache. A noter que l'approche doit être forcement récursive.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21

public class Fibonacci extends RecursiveTask<Integer> { public static void main(final String[] args) { final ForkJoinPool p = new ForkJoinPool(); final Fibonacci f = new Fibonacci(1_000_000_000); p.execute(f); } final int n; Fibonacci(final int n) { this.n = n; } @Override protected final Integer compute() { if (this.n <= 1) { return this.n; } final Fibonacci f1 = new Fibonacci(this.n - 1); f1.fork(); final Fibonacci f2 = new Fibonacci(this.n - 2); return f2.compute() + f1.join(); } }

Voila un petit tour d'horizon de java 7, on approche de la dernière version officiellement sortie, la version 9 mais il nous reste encore la version 8 qui a apporté une nouvelle fois de nouveaux concepts très important.

Informations complementaires sur java 7