Développement formel de systèmes automatisés, Formal development of automated systems

Olfa Mosbahi-Khalgui

Description

Sous la direction de Jacques Jaray, Samir Ben Ahmed
Thèse soutenue le 21 février 2008: INPL
Le travail de thèse présente une méthode de développement de systèmes automatisés basée sur les méthodes formelles B et TLA+. Le développement par raffinement est au cœur de la méthode proposée. Un système automatisé est modélisé par deux composants, un contrôlé formé par le dispositif physique et son environnement et un contrôleur pilotant ce dernier. Il est exprimé par un produit synchronisé sur les actions de ces deux composants. La première contribution de la thèse concerne la proposition d'une approche qui combine le B événementiel et le langage de modélisation TLA+ pour la vérification des propriétés de vivacité. Nous définissons une extension syntaxique et sémantique du B événementiel permettant d'exprimer des propriétés de vivacité. Nous développons un prototype pour la transformation d'un modèle B en un module TLA+ sur lequel nous effectuons la preuve des propriétés de vivacité avec le model checker TLC. Pour la vérification de ce type de propriétés sur des systèmes infinis, nous proposons l'utilisation des diagrammes de prédicats qui sont des abstractions des systèmes modélisés en TLA+. La deuxième contribution est la proposition d'une technique pour représenter explicitement le temps en B événementiel. Cette technique s'appuie sur la réalisation d'un entrelacement entre un processus qui gère le temps avec les autres processus du système. Le temps modélisé est discret et son écoulement est modélisé par des événements. Cette approche est assez différente des systèmes temporisés où l'on considère que le temps s'écoule indépendamment du système. Dans la troisième contribution, nous proposons une approche de développement des systèmes automatisés en utilisant la technique de composition où il s'agit de développer conjointement le contrôleur et le composant physique qu'il contrôle et appliquer le raffinement aussi bien sur le contrôleur que le contrôlé. Le raffinement est une technique de base des méthodes que nous proposons et si notre objectif est de construire des contrôleurs corrects, le critère de correction porte sur le comportement du système automatisé qui résulte de la composition du contrôleur et du contrôlé. Nous présentons également un théorème de compositionnalité qui indique sous quelles conditions il est possible de déduire que le composé des raffinements des contrôleur et contrôlé est un raffinement du composé des contrôleur et contrôlé abstraits. La dernière contribution porte sur la définition, la preuve et l'utilisation d'un patron de raffinement pour les processus continus dans des systèmes de production manufacturière. Ce type de patron prouvé permet d'utiliser l'abstraction discrète de l'effet d'un processus continu agissant pendant un certain temps
-Modélisation
-Diagrammes de prédicats
-TLA+
-B événementiel
-Systèmes automatisés
-Patrons de conception
-Composition
-Raffinement
-Vérification
This thesis deals with the development of automated systems while following the formal methods B and TLA+. We propose a formal methodology based on the refinement paradigm to specify and verify the system that we model by two components: the controlled system representing the physical device and its environment, and the controller that controls the system. A synchronised product on the actions of these two components is applied to specify the automated system. As a first contribution, we propose an approach combining the event B method and the language TLA+ in order to verify liveness properties defined in user requirements. Inspired by the temporal logic of actions TLA, we first extend the event B notation to specify liveness properties and we give semantics of this extended syntax over traces. Second, we give transformation rules from a temporal B model into a TLA+ module. We present, in particular, our prototype system called B2TLA+, that we have developed to support this transformation. To consider infinite systems, we use predicate diagrams as abstractions of systems modelled with TLA+. To consider the real-time concept in automated systems, we propose as a second contribution a technique explicitly representing time in B event systems. This technique is based on an interleaving between any event handling time and the other system events. By considering the well known co-design technique, we propose as a third contribution a refinement-based composition technique keeping a separation between controller and controlled systems in order to build correct automated systems satisfying user requirements. We prove a compositionality theorem with respect to refinement to get an efficient approach to verify the refinement of a synchronized composition between components. We verify the refinement of a synchronized composition by verifying separately the refinement of each component. Finally, we define, prove and use in a case study as a fourth contribution the concept of a refinement pattern for continuous processes in manufacturing systems. Such proven pattern allows us to use the discrete abstraction of the effect of continuous processes operating for a while
-Modelling
-Predicate diagrams
-TLA+
-Verification
-Composition
-Design patterns
-Automated systems
-Event B method
-Refinement
Source: http://www.theses.fr/2008INPL007N/document

Sujets

• Modélisation
• Patron de conception
• Raffinement
• Vérification

Informations

• Publié par: Thesee
• Nombre de lectures: 134
• Langue: Français
• Poids de l'ouvrage: 3 Mo

Extrait

AVERTISSEMENT



Ce document est le fruit d’un long travail approuvé par le jury de
soutenance et mis à disposition de l’ensemble de la communauté
universitaire élargie.
Il est soumis à la propriété intellectuelle de l’auteur au même titre que sa
version papier. Ceci implique une obligation de citation et de
référencement lors de l’utilisation de ce document.
D’autre part, toute contrefaçon, plagiat, reproduction illicite entraîne une
poursuite pénale.

Contact SCD INPL : [e-mail]




LIENS




Code de la propriété intellectuelle. Articles L 122.4
Code de la propriété intellectuelle. Articles L 335.2 – L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm
Institut National Facult´e Des Sciences de Tunis
Polytechnique de Lorraine Universit´e Tunis-El Manar
D´epartement de formation doctorale en informatique
´Ecole doctorale IAEM Lorraine
D´eveloppement formel des syst`emes
automatis´es
`THESE
pr´esent´ee et soutenue publiquement le 21 f´evrier 2008
pour l’obtention du
Doctorat de
l’Institut National Polytechnique de Lorraine
l’Universit´e Tunis-El Manar
(sp´ecialit´e informatique)
par
Olfa MOSBAHI
Composition du jury
Pr´esident : Stephan Merz Directeur de recherche, INRIA, LORIA
Rapporteurs : Jacques Julliand Professeur, Universit´e de Franche-comt´e
Riadh Robbana Maˆıtre de conf´erence, HDR, Ecole polytechnique de Tunis
Examinateurs : Jacques Jaray Professeur, Institut National Polytechnique de Lorraine
Samir Ben Ahmed Facult´e des Sciences de Tunis
Nejib Ben Hadj Alouane Maˆıtre de conf´erence, HDR, ENSI de Tunis
Laboratoire Lorrain de Recherche en Informatique et ses Applications — UMR 7503Mis en page avec la classe thloria.Remerciements
J’adresse mes plus vifs remerciements à mes directeurs de thèse M. Jacques Jaray, professeur
à l’INPL, et M. Samir Ben Ahmed, professeur à la FST, pour leur encadrement de qualité dont
il m’ont fait bénéficier aimablement, pour leur disponibilité et leur soutien permanents, pour la
patience avec laquelle ils ont suivi et corrigé mon travail. Qu’ils trouvent ici l’expression de ma
profonde gratitude et de ma reconnaissance.
Je tiens également à remercier M. Dominique Mery, professeur à l’UHP, responsable de
l’équipe MOSEL pour m’avoir accueillie au sein de son équipe, pour m’avoir procuré d’excel-
lentes conditions de travail ainsi que pour ses encouragements.
J’exprime mes sincères remerciements à M. Stephan Merz, directeur de recherche INRIA,
pour ses conseils judicieux, ainsi que ma gratitude pour son aide et son soutien qu’il a bien
voulu manifester à mon égard, me prodiguant les bienveillantes directives dont j’avais besoin
pour mener à bien ce travail.
Je tiens à remercier Mme Leila Jemni Ben Ayed d’avoir participé à l’encadrement de la thèse
et dont je suis reconnaissante, pour son soutien, ses conseils et ses remarques intéressantes.
Je remercie vivement M. Jacques Julliand et M. Riadh Robbana pour leur judicieux travail
d’évaluationdelathèse,leurscommentairesquiontcontribuéàl’améliorationdecedocumentet
leursremarquestrèsconstructives.JeremercieaussiM.NejibBenHadj-Alouaned’avoirexaminé
ce travail et pour ses intéressantes remarques dont je dois prendre en compte dans mes futurs
travaux.
Je tiens à remercier tous les membres de l’équipe MOSEL, avec qui travailler fut toujours un
plaisir en raison de leur disponibilité et de leur convivialité. Merci à Dominique Cansell, Joris
Rehm, Loïc Fejoz et Nazim Benaïssa. Merci aussi aux assistantes Josiane Reffort et Roxane
Auclair pour leurs services administratifs de qualité et à Nadine Beurné pour son aide dans le
règlement des problèmes atifs.
Touteslespersonnesm’ayantpermisdemeneràbiencetravailsontassuréesdemagratitude.
12Je dédie ce travail,
à mes parents...
à mon mari Mohamed...
à mon Cher Mohamed Aziz...
à toute la famille...
34Résumé
Le travail de thèse présente une méthode de développement de systèmes automatisés basée
+sur les méthodes formelles B et TLA . Le développement par raffinement est au cœur de la
méthode proposée. Un système automatisé est modélisé par deux composants, un contrôlé formé
parledispositifphysiqueetsonenvironnementetuncontrôleurpilotantcedernier.Ilestexprimé
par un produit synchronisé sur les actions de ces deux composants.
La première contribution de la thèse concerne la proposition d’une approche qui combine
+le B événementiel et le langage de modélisation TLA pour la vérification des propriétés de
vivacité. Nous définissons une extension syntaxique et sémantique du B événementiel permettant
d’exprimerdespropriétésdevivacité.Nousdévelopponsunprototypepourlatransformationd’un
+modèle B en un module TLA sur lequel nous effectuons la preuve des propriétés de vivacité
avec le model checker TLC. Pour la vérification de ce type de propriétés sur des systèmes infinis,
nous proposons l’utilisation des diagrammes de prédicats qui sont des abstractions des systèmes
+modélisés en TLA .
La deuxième contribution est la proposition d’une technique pour représenter explicitement
le temps en B événementiel. Cette technique s’appuie sur la réalisation d’un entrelacement entre
un processus qui gère le temps avec les autres processus du système. Le temps modélisé est
discret et son écoulement est modélisé par des événements. Cette approche est assez différente
des systèmes temporisés où l’on considère que le temps s’écoule indépendamment du système.
Dans la troisième contribution, nous proposons une approche de développement des systèmes
automatisés en utilisant la technique de composition où il s’agit de développer conjointement
le contrôleur et le composant physique qu’il contrôle et appliquer le raffinement aussi bien sur
le contrôleur que le contrôlé. Le raffinement est une technique de base des méthodes que nous
proposons et si notre objectif est de construire des contrôleurs corrects, le critère de correction
porte sur le comportement du système automatisé qui résulte de la composition du contrôleur
et du contrôlé. Nous présentons également un théorème de compositionnalité qui indique sous
quelles conditions il est possible de déduire que le composé des raffinements des contrôleur et
contrôlé est un raffinement du composé des contrôleur et contrôlé abstraits.
La dernière contribution porte sur la définition, la preuve et l’utilisation d’un patron de
raffinement pour les processus continus dans des systèmes de production manufacturière. Ce
type de patron prouvé permet d’utiliser l’abstraction discrete de l’effet d’un processus continu
agissant pendant un certain temps.
Mots-clés: Modélisation, Vérification, Raffinement, Composition, Patrons de conception, Sys-
+tèmes automatisés, B événementiel, TLA , Diagrammes de prédicats.
5Abstract
This thesis deals with the development of automated systems while following the formal
+methods B and TLA . We propose a formal methodology based on the refinement paradigm to
specify and verify the system that we model by two components :the controlled system repre-
senting the physical device and its environment, and the controller that controls the system. A
synchronisedproductontheactionsofthesetwocomponentsisappliedtospecifytheautomated
system.
As a first contribution, we propose an approach combining the event B method and the
+languageTLA inordertoverifylivenesspropertiesdefinedinuserrequirements.Inspiredbythe
temporal logic of actions TLA, we first extend the event B notation to specify liveness properties
and we give semantics of this extended syntax over traces. Second, we give transformation rules
+from a temporal B model into a TLA module. We present, in particular, our prototype system
+called B2TLA , that we have developed to support this transformation. To consider infinite
+systems, we use predicate diagrams as abstractions of systems modelled with TLA .
To consider the real-time concept in automated systems, we propose as a second contribu-
tion a technique explicitly representing time in B event systems. This technique is based on an
interleaving between any event handling time and the other system events.
By considering the well known co-design technique, we propose as a third contribution a
refinement-based composition technique keeping a separation between controller and controlled
systems in o