• Langue : Français
• Discipline : Productique, automatique et informatique industrielle
• Identifiant : 2000LIL10067
• Type de thèse : Doctorat
• Date de soutenance : 01/01/2000

Résumé en langue originale

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.