Université Lille1 - Sciences et Technologies Du cahier des charges aux spécifications formelles : une méthode basée sur les réseaux de Pétri de haut niveau From informal to formal Comportement dynamique Spécifications formelles 005.3 Génie logiciel Spécifications Petri, Réseaux de Logiciels Développement Méthode B (informatique) Text Electronic Thesis or Dissertation fr Aujourd'hui, un des points cruciaux dans le développement des logiciels critiques est le passage de l'informel au formel. Le but de cette thèse est de définir ici une méthodologie de développement permettant un passage plus intuitif du cahier de charges (spécifications informelles) aux spécifications formelles d'un système, en tenant compte de son comportement dynamique. Cette méthodologie se base sur l'utilisation d'un modèle lisible et expressif. Notre choix s'est donc porté les réseaux de Pétri de haut niveau qui combinent trois qualités importantes : la représentation graphique, le comportement dynamique et l'abstraction des traitements. Elle peut se décomposer en plusieurs phases. D'abord nous tenterons une représentation graphique du cahier des charges par le réseau de Pétri proprement dit. Puis la phase d'interprétation du cahier des charges où nous annoterons le réseau de Pétri obtenu par du langage naturel. La troisième phase, dite de formalisation, transformera les annotations du réseau de Pétri en formules mathématiques (contraintes). Enfin nous terminerons par une phase de traduction automatique du réseau de Pétri en machine abstraite b et nous poursuivrons par une procédure b classique. application/pdf 1 : 1 Mo https://pepite-depot.univ-lille.fr/RESTREINT/Th_Num/2000/50376-2000-149.pdf Bon Philippe 1900-01-01 059847441 2000LIL10067 2000-01-01 Productique, automatique et informatique industrielle Université Lille1 - Sciences et Technologies 026404184 Doctorat non oui Yim Pascal 059847654 Gentina Jean-Claude 059857501 ddc:000 ASCII PDF 9999 restriction 2012-01-01 9999-01-01 restriction 2012-01-01 9999-01-01