[MODEL2012] Comparaison sémantique de langages haut niveau – Synthèse

Suite à des difficultés techniques avec Eclipse, il ne m’a pas été possible de réaliser les modèles AADL tant attendus avec l’Etoile de la Mort. J’espère néanmoins pouvoir répondre à mon engagement durant les prochains mois, où je travaillerai sur des stations de travail préconfigurées avec tous les outils nécessaires.

Au cours de cette veille, nous avons fait un état de l’art de la modélisation/vérification de langages haut niveau répandus comme UML/SysML/AADL.

Nous avons également constaté que le manque de formalisme de ces modèles implique de passer par des outils annexes pour lancer une analyse formelle. Mais ce défaut ne doit pas être vu comme une vraie limite : UML n’est pas fait pour de l’analyse formelle !

Ainsi, nous avons différents langages, et différents buts. L’industrie s’est emparée de ces outils, et a voulu étendre leurs champs de possibilités : cette opération entraîne forcément de la complexité.

Pour résumer notre étude (paragraphe généralement noté TL;DR) :

  • UML est fait pour diffuser l’information, en particulier pour le milieu du logiciel (software) [1] ;
  • UML est plus facile à lire qu’à écrire ;
  • SysML sert à ajouter une partie matérielle (hardware) [2] ;
  • AADL apporte des degrés d’interaction entre couches software et hardware, et apporte le ciment des briques UML/SysML [3] ;
  • Une analyse formelle est possible avec Tina, en passant d’abord par Fiacre [4] ;
  • La boîte à outils du parfait ingénieur système sera formée à partir d’Eclipse (plugins OSATE + Topcased), et de Tina [4].
Pour les étudiants en informatique intéressés par le web, les plus curieux auront remarqué l’importance des notions de scalabilité dans les systèmes d’information : un système doit s’adapter au nombre d’utilisateurs. Cela nécessite d’utiliser des architectures spécifiques redondantes, dont les champions sont Amazon Web Services, Heroku mais aussi le français Clever-Cloud.
Cet avis n’engage que moi, mais il n’existe pas actuellement de systèmes de modélisation de telles infrastructures garantissant un taux de service de 100% à partir d’une analyse formelle. Pourtant, ces langages permettant de lier des architectures software et hardware, et je suis donc convaincu qu’une étude de l’application de ces méthodes aux systèmes d’information apporterait des conclusions intéressantes pour l’optimisation de ces infrastructures… Vers une révolution du cloud computing ?
Vous pouvez également retrouver le Séminaire bibliographique réalisé dans le cadre de cette étude avec le lien suivant et les slides de présentation.
[1] http://veille-techno.blogs.ec-nantes.fr/index.php/2012/11/17/model-2012-uml-un-langage-pour-les-amener-tous-et-dans-les-tenebres-les-lier/

[2] http://veille-techno.blogs.ec-nantes.fr/index.php/2012/12/09/model2012-sysml-se-centrer-pour-regner/

[3] http://veille-techno.blogs.ec-nantes.fr/index.php/2013/01/13/model2012-aadl-ou-vers-le-model-checking/

[4] http://veille-techno.blogs.ec-nantes.fr/index.php/2013/03/08/model2012-verification-formelle/

Licence Creative Commons
Comparaison sémantique de langages haut niveau de Maxime Alay-Eddine est mis à disposition selon les termes de la licence Creative Commons Attribution 3.0 non transposé.

[MODEL2012] Vérification formelle

Les articles précédents traitaient des problèmes de modélisation, mais à quelles fins ? Dans une époque où l’informatique joue un rôle prépondérant dans les travaux de conception, nous avons la possibilité de traiter et de vérifier des systèmes complexes avant leur réalisation, afin de corriger d’éventuelles erreurs sans être passé par une phase de production. Cette technique engendre un gain important d’argent, mais permet aussi d’assurer la fiabilité des systèmes critiques utilisés notamment dans l’armement.

La théorie derrière ce type d’étude est la vérification formelle, qui consiste à vérifier des propriétés de façon formelle, c’est-à-dire mathématique. Nous réduisons donc l’ensemble des données étudier à des états et relations logiques.

Appliquons ces études à notre cas : nous avons des modèles UML, SysML, et AADL, et souhaitons leur appliquer des méthodes formelles. Nous ne pouvons effectuer directement ces calculs ! Il faut donc utiliser un langage intermédiaire, obtenu à l’aide d’outils adaptés, comme Fiacre (Format Intermédiaire pour les Architectures de Composants Répartis Embarqués) [1].

Fiacre permet de traduire une multitude de langages de haut niveau en un langage unique analysable par méthodes formelles. Il ne se réduit donc pas aux langages cités, et subit régulièrement des mises à jour lui permettant d’élargir sa gamme d’entrée.

Après analyse, nous obtenons un système décrit à partir de deux entités :

  • Les processus : ils décrivent le comportement des composants séquentiels ;
  • Les composants : ils décrivent un système comme une composition de processus.
Le lecteur désireux d’obtenir plus d’informations pourra regarder Topcased [2], un plugin Eclipse permettant de lire et traduire les modèles de travail.
Une fois ce langage “intermédiaire” obtenu, nous devons l’analyser. Nous nous concentrerons ici sur Tina [3].
Tina est une boîte à outils permettant d’analyser et d’éditer des réseaux de Petri [4]. Ces réseaux sont des outils complexes qui ne seront pas développés ici, et nous nous concentrerons sur l’essentiel : l’analyse du langage obtenu avec Fiacre.
Une analyse avec Tina est définie à partir d’éléments logiques. Soit p, q des formules logiques, nous avons :
  • —p correspond à la négation de p
  • p= nq correspond à la conjonction de p et q
  • ()p sera vraie si p est vérifiée à l’état suivant (opérateur Next)
  • []p sera vraie si p est vérifiée dans tout état du chemin étudié (opérateur Always)
  • <> p sera vraie si p est vérifiée dans un état futur du chemin étudié (opérateur Eventually)
  • pUq sera vraie si p est vérifiée jusqu’à ce que q soit vérifiée (opérateur Until)
En combinant cette notation avec les processus Fiacre process1, process2, possédant les états w_process_1 w_process_2 (processus en attente), et cs_process_1, cs_process_2 (processus en zone critique), nous avons [5] :
  • [](cs_process 1 + cs_process 2 < = 1) correspond à l’exclusion mutuelle : les processus 1 et 2 ne peuvent jamais être en même temps dans leur zone critique ;
  • []((w_process 1 =><> cs_process 1) /\ (w_process 2 =><> cs_process 2)) correspond à la condition de non-famine : si le processus 1 ou 2 entre en état d’attente, il entrera forcément en zone critique par la suite.
Une analyse Tina consiste donc à vérifier une propriété correspondant aux exigences du système modélisé (non-famine, exclusion mutuelle, délais bornés, etc.).
L’analyse classique des modèles UML/SysML/AADL passera donc par Fiacre et Tina, Fiacre n’étant qu’un intermédiaire transparent pour l’utilisateur.
Ces démarches peuvent paraître complexes, mais sont heureusement accessibles via deux environnements logiciels :
  • Eclipse, avec les plugins OSATE/Topcased pour la partie UML/SysML/AADL => Fiacre ;
  • Tina pour faire l’analyse du langage Fiacre.
Bien que très mathématiques, de nombreux travaux sont en cours pour rendre l’ensemble utilisable par le néophyte [1][5]. Il reste à noter que cette démarche est en évolution perpétuelle, pour en améliorer les capacités techniques : il n’est actuellement pas possible de modéliser des systèmes où le nombre d’instance change au cours du temps, malgré le fait que les calculs parallèles soient de plus en plus représentés dans l’industrie et que cette architecture soit désormais souvent utilisée.
[1] Bernard Berthomieu, Jean-Paul Bodeveix, Patrick Farail, Mamoun Filali, Hubert Garavel, Pierre Gaufillet, Frederic Lang, and François Vernadat. Fiacre : an Intermediate Language for Model Verification in the Topcased Environment. In ERTS 2008 , Toulouse, France, 2008.
[2] http://www.topcased.org/
[3] B. Berthomieu, P.-O. Ribet, and F. Vernadat. The tool tina – construction of abstract state spaces for petri nets and time petri nets. International Journal of Production Research , 42(14) :2741–2756, 2004.
[4] http://fr.wikipedia.org/wiki/R%C3%A9seau_de_Petri
[5] Bernard Berthomieu, Jean-Paul Bodeveix, Christelle Chaudet, Silvano Zilio, Mamoun Filali, and François Vernadat. Formal verification of aadl specifications in the topcased environment. In Proceedings of the 14th Ada-Europe International Conference on Reliable Software Technologies , Ada-Europe ’09, pages 207–221, Berlin, Heidelberg, 2009. Springer-Verlag.
Licence Creative Commons
Comparaison sémantique de langages haut niveau de Maxime Alay-Eddine est mis à disposition selon les termes de la licence Creative Commons Attribution 3.0 non transposé.