Master 2014 2015
Stages de la spécialité SAR
Compilation de spécifications formelles « de haut niveau » vers Guarded Action Language (GAL) pour une vérification efficace


Site :Trac-Compilation de spécifications formelles « de haut niveau » vers Guarded Action Language (GAL) pour une vérification efficace
Lieu :LIP6
Encadrant : Fabrice.Kordon@lp6.fr, Yann.Thierry-Mieg@lip6.fr
Dates :mars-Août
Rémunération :475€/mois (gratification classique)
Mots-clés : Master SAR, autre qu’ATIAM

Description

Introduction

Dans l’industrie, les logiciels assurent un nombre grandissant de fonctions critiques (transports, télécommunications, etc.). Les enjeux humains sont tels qu’il est nécessaire de pouvoir garantir les propriétés des systèmes. Ce besoin a conduit à la mise en place de méthodologies basés sur des modèles qui permet d’abstraire le coté programmatique du logiciel pour se focaliser sur les aspects comportementaux. Le modèle doit être défini très tôt dans la conception et introduire une représentation qui doit être valide tout au long du développement du produit. A partir de cette représentation de nombreux outils de génération de code ont été mis en place ce qui permet d’assurer une cohérence entre le modèle et le code.

Cependant rien ne garantit que le système modélisé est correct et que son fonc- tionnement n’est pas erroné. Actuellement la vérification des logiciels (qu’ils aient été produits par génération de code ou non) se fait essentiellement via l’utilisation de scé- narios de tests ou par simulation. Ces mécanismes permettent uniquement d’assurer que le comportement nominal semble correct, et que certains cas d’erreurs soient évi- tés. Ces méthodes ne sont pas satisfaisantes car il est très difficile d’être exhaustif et certaines applications ne se prêtent pas à de telles méthodes (c’est typiquement le cas des systèmes répartis).

Le model-checking se présente comme une alternative possible car il explore de façon systématique l’ensemble des comportements possibles du modèle. Il est cepen- dant soumis au problème classique de l’explosion combinatoire, en particulier dans le cas de systèmes répartis. Pour combattre cette explosion, différentes solutions ont été proposées mais les activer implique une bonne connaissance des techniques ainsi ci- tées. Pour palier ce problème, la notion de langage pivot, assurant la jonction entre des langages de haut niveau manipulables par des ingénieurs, et des bibliothèques de véri- fication efficace, constitue une piste intéressante. L’équipe MoVe du LIP6 a développé un tel langage à titre expérimental : Guarded Action Language (GAL) [2].

Objectif du stage

le langage GAL est assez récent et nous souhaitons l’expérimenter dans des contextes différents. Des études sur différents types de réseaux de Petri [4] (colorés, temporels), Clock Constrained Specification Language (CCSL, [1]) et sur des Domain Specific Languages sont en cours.

L’objectif de ce stage consiste à s’intéresser à de tels notations de haut niveau. Deux sont a priori visées :

  • les Symmetric Nets with Bag [5] qui sont des réseaux de Petri de haut niveau,
  • LOTOS au travers d’un export de l’outil CADP [3] (développé au LIG à Gre- noble) sous la forme de réseaux de Petri interprétés.

Pour cela, l’idée est d’écrire un compilateur de ces notations de haut niveau vers le langage GAL et d’invoquer ensuite l’outil capable de les analyser de manière efficace.

Travail à réaliser

L’objectif de ce stage est de réaliser un compilateur vers GAL de ces différentes notations afin de valider leur utilisation comme base de vérification dans des contexte différents. Ce compilateur s’appuiera sur la bibliothèque de fonctions libits (voir le site htp ://ddd.lip6.fr) qui a déjà démontré son efficacité.

Les Symmetric Nets with Bag ont déjà fait l’objet d’une étude préliminaire ayant démontré la faisabilité (mais aucun test de performance n’a pu être effectué à ce stade).

La traitement des réseaux de Petri interprétés issus de LOTOS via l’outil CADP permettrait, entres autres, d’accéder à un jeu de tests considérable (plusieurs milliers de modèles) permettant une évaluation solide de libits.

Pré-requis et apports du stage

Un certain goût pour les méthodes formelles, associé à une bonne capacité d’abs- traction sont souhaités. Une aisance dans le développement d’outils sera appréciée.

Le candidat devra faire preuve d’autonomie et d’initiative afin de surmonter les difficultés techniques du stage.

Ce stage sera en contre-partie l’occasion pour le stagiaire :

  • de s’insérer dans un projet de recherche portant sur un domaine dont les contributions fondatrices sont en cours d’élaboration ;
  • de produire un logiciel libre dont le cadre conceptuel et formel est inédit ;
  • d’approfondir sa connaissance des les méthodes formelles ;
  • d’établir une connexion avec un sujet de recherche qui pourrait déboucher sur une thèse.

Bibliographie

[1] Xiaohong Chen, Jing Liu, Frédéric Mallet, and Zhi Jin. Modeling timing requi- rements in problem frames using ccsl. In 18th Asia Pacific Software Engineering Conference, pages 381–388. IEEE, 2011

[2] M. Colange, S. Baarir, F. Kordon, and Y. Thierry-Mieg. Towards Distributed Soft- ware Model-Checking using Decision Diagrams. In 25th International Conference on Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pages 830–845, Rome, Italy, March 2013. Springer.

[3] Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. CADP 2011 : A Toolbox for the Construction and Analysis of Distributed Processes. International Journal on Software Tools for Technology Transfer, 15(2) :89–107, 2013.

[4] C. Girault and R. Valk. Petri Nets for Systems Engineering. Springer Verlag - ISBN : 3-540-41217-4, 2003.

[5] S. Haddad, F. Kordon, L. Petrucci, J-F. Pradat-Peyre, and N. Trèves. Efficient State-Based Analysis by Introducing Bags in Petri Net Color Domains. In 28th American Control Conference (ACC’09), pages 5018–5025, St-Louis, USA, June 2009. Omnipress IEEE.