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.
Ce document a été traduit de LATEX par HEVEA