Encadrement : Christine Choppy, Micaela Mayero, Laure Petrucci

Lieu : LIPN, CNRS UMR 7030
Université Paris13
99 avenue Jean-Baptiste Clément
93430 VILLETANEUSE

Contacts : {Christine.Choppy, Micaela.Mayero, Laure.Petrucci}@lipn.univ-paris13.fr

La vérification et la validation de systèmes informatiques constitue aujourd'hui un enjeu crucial. C'est en particulier le cas pour les systèmes critiques dont les pannes peuvent avoir des conséquences irréversibles et dramatiques sur leur environnement (explosion d'Ariane 5, systèmes de suivi médical, systèmes de missions avioniques [PKBQ03], …). Dans ce cadre, une solution consiste à concevoir une spécification comportementale du système étudié, à l'aide de méthodes formelles, puis à analyser le modèle obtenu.

Il existe divers modèles pour les systèmes critiques tels que : les automates, les réseaux de Petri, …

Des études poussées ont été effectuées avec l'outil Design/CPN [CPNb], pour les réseaux de Petri hiérarchiques de haut niveau. Des études de cas ont montré l'importance de ces méthodes de validation dans différents secteurs d'applications : par exemple la santé, les centrales nucléaires, la téléphonie mobile [CPNa]. Les réseaux de Petri de haut niveau sont composés d'un réseau de Petri spécifiant les interactions entre les différentes composantes du système, et d'une modélisation des données, par exemple par des spécifications de types abstraits algébriques.

La démarche de modélisation et validation part généralement d'une vision abstraite du système considéré puis, une fois celui-ci validé, remplace des parties par une modélisation plus concrète. C'est ce que l'on appelle du raffinement. Des techniques de raffinement ont été proposées dans le cadre des réseaux de Petri de haut niveau [LL01], mais elles ne tiennent compte que de la structure de réseau de Petri, et non des données manipulées. D'autre part, des travaux [ONS96] portent sur le raffinement de spécifications algébriques.

L'objet du stage est d'étudier la combinaison de ces deux approches et de les intégrer pour pouvoir raffiner des réseaux de Petri de haut niveau en considérant à la fois la structure de synchronisation déterminée par le réseau de Petri et les données manipulées définies dans la spécification algébrique. On devra également montrer dans quelle mesure cette nouvelle approche préserve les propriétés du système abstrait au niveau concret, c'est-à-dire si ces propriétés sont complètement préservées ou, dans le cas contraire, quelle est la partie supplémentaire à vérifier, sachant que l'on souhaite exploiter au mieux les résultats obtenus sur le modèle abstrait.

Références

[CPNa]

Examples of Industrial Use of CP-nets. http://www.daimi.au.dk/CPnets/intro/example_indu.html.

[CPNb]

Design/CPN online. http://www.daimi.au.dk/designCPN.

[LL01]

C. Lakos and G. Lewis. Incremental state space construction of coloured Petri nets. In Proc. 22nd Int. Conf. Application and Theory of Petri Nets (ICATPN'01), Newcastle, UK, June 2001, volume 2075 of Lecture Notes in Computer Science, pages 263–282. Springer, 2001.

[ONS96]

F. Orejas, M. Navarro, and A. Sanchez. Algebraic implementation of abstract data types: a survey of concepts and new compositionality results. Mathematical Structures in Computer Science, pages 33–67, 1996.

[PKBQ03]

L. Petrucci, L. M. Kristensen, J. Billington, and Z. H. Qureshi. Developing a formal specification for the mission system of a maritime surveillance aircraft. In Proc. 3rd Int. Conf. on Application of Concurrency to System Design (ACSD'03), Guimarães, Portugal, June 2003, pages 92–101. IEEE Comp. Soc. Press, 2003.

Ce document a été traduit de L^AT_EX par H^EV^EA