Sujet de stage
Une méthode d'analyse et spécification pour les systèmes complexes avec des réseaux de Petri de haut niveau et des spécifications algébriques


Encadrement : Christine Choppy - Laure Petrucci

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


Contacts : {Christine.Choppy, Laure.Petrucci}@lipn.univ-paris13.fr
http://www-lipn.lipn.univ-paris13.fr/~choppy/ , ~petrucci


Le développement de systèmes informatiques complexes nécessite une conception préalable qui puisse garantir au mieux que le système que l'on construit satisfera les contraintes nécessaires à son bon fonctionnement. Pour ce faire, on commence par spécifier formellement le système.

Les spécifications formelles restent difficile à écrire car les systèmes à développer actuellement sont d'une assez grande complexité. Il est donc nécessaire de proposer des méthodes facilitant la démarche d'analyse et de spécification des systèmes complexes.

Dans [CR05] une méthode est proposée et illustrée par le développement de spécifications écrites dans un langage de spécification algébrique. Cette méthode est basée sur les caractéristiques sémantiques souhaitées pour guider vers des spécifications pertinentes. Une distinction est effectuée entre systèmes dynamiques simples, structurés, et types de données. Toutefois, cette méthode est a priori assez générale pour pouvoir être utilisée avec d'autres types de spécification. Les réseaux de Petri sont un formalisme utilisé pour différents types d'applications réactives, telles que les protocoles de communication, les téléphones portables, les ateliers flexibles ... Les paradigmes des réseaux de Petri sont très différents de ceux des spécifications algébriques, mais une méthode de modélisation s'avère également nécessaire. Nous nous intéressons ici aux réseaux de Petri colorés qui sont des réseaux de Petri "de haut niveau", combinant une structure de contrôle de type réseau de Petri et partie données exprimée dans un langage de programmation ou sous forme de types abstraits algébriques.

Une première approche [CP04] montre comment utiliser les principes méthodologiques pour un système de pilotage de train électrique [BP01]. L'objectif est donc de poursuivre ce travail et de l'étendre à travers les enseignements tirés d'une étude de cas plus importante, portant sur la spécification de systèmes avioniques ou de systèmes pour les téléphones portables. On devra notamment étudier comment effectuer une structuration modulaire des réseaux pour la spécification d'un système dynamique complexe.

On cherchera à concevoir une méthode pour aider à la spécification de systèmes complexes à l'aide de réseaux de Petri colorés. Ceci permettra de fournir des guides précis en vue d'obtenir une spécification claire, bien structurée et flexible.

Cette méthode doit fournir des guides qui permettent : d'attaquer des systèmes complexes et de les décomposer en sous-systèmes, de spécifier les sous-systèmes en réseaux de Petri colorés (places, transitions étiquetées par des termes et éventuellement munies de gardes, données manipulées, ...) de spécifier la composition des sous-systèmes pour obtenir le système global de spécifier les propriétés souhaitées pour le système global et pour les sous-systèmes.

Ces guides doivent également aider à une " bonne " utilisation du formalisme pour produire des spécifications dont les propriétés induites par la sémantique correspondent aux classes souhaitées. Des notations graphiques pour la composition seront proposées. Tous ces éléments peuvent aussi conduire à des guides d'utilisation des outils d'édition et d'analyse existants.

Références

[BP01]
G. Berthelot and L. Petrucci. Specification and validation of a concurrent system: An educational project. Journal of Software Tools for Technology Transfer, 3(4):372–381, 2001.
[CP04]
Christine Choppy and Laure Petrucci. Towards a Methodology for Modelling with Petri Nets. In K. Jensen, editor, Fifth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, pages 39–56, Aarhus, Denmark, October 2004. DAIMI PB - 570, ISSN 0105-8517.
[CR05]
Christine Choppy and Gianna Reggio. A Formally Grounded Software Specification Method. Journal of Logic and Algebraic Programming, Elsevier, 2005.

Ce document a été traduit de LATEX par HEVEA