Conception d'un atelier pour l'algèbre de processus mCRL2

Défense de mémoire de Jeremy Vander Auwera

Via ce lien

 

Le mCRL2 est une algèbre des processus. Elle possède des outils qui permettent d'aider au raisonnement et à l'analyse de spécifications. Cependant, ils ont tous tendance à modifier la spécification et à ne pas mentionner les processus mais plutôt de se concentrer uniquement sur les actions. Ces deux inconvénients, retrouvés sur tous les outils proposés par mCRL2, proviennent de la transformation de la spécification sous une forme linéaire. Ce mémoire a pour but de développer un outil plus dynamique et qui ne passera pas par cette forme linéaire. Une analyse d'une application qui a été créée sans passer par la forme linéaire est réalisée confirmant les motivations de ne pas utiliser cette forme. Cependant, l'analyse de cette application révèle un manque de dynamisme et se concentre fortement sur les actions en mettant de côté les processus. L'application créée affiche un ascenseur par processus possédant un étage par action possible. Les ascenseurs se déplacent pour amener du dynamisme. La trace des actions exécutées peut se faire par processus. Un retour en arrière est possible pendant l'exécution. Et bien d'autres fonctionnalités palliant les défauts retrouvés au sein des outils analysés. L'aspect technique comprenant un scindement entre le backend et le frontend repose sur les technologies : Scala, Typescript, Angular et Spring. Il offre des points d'entrée API qui permettent notamment de récupérer toutes les actions exécutables possibles au fur et à mesure de l'exécution. Ce point d'entrée est créé pour permettre d'être réutilisé pour d'autres affichages dynamiques d'exécution de spécification. L'outil créé pousse à la réflexion de la forme linéaire en se demandant si les défauts qu'elle engendre ne valent pas le coup d'être évité au profit des avantages de ne pas l'utiliser. Conscient que cette dernière est au cœur de tous les outils proposés par mCRL2, le présent mémoire suggère une analyse plus poussée de l'utilité de la forme linéaire pour comprendre les tenants et les aboutissants de l'utilisation de cette forme.

Contact : Isabelle Daelman - isabelle.daelman@unamur.be
Télecharger : vCal