Ces cinquante dernières annéees, les ordinateurs ont occupé une place toujours plus importante dans notre vie quotidienne. On les retrouve aujourd’hui présents dans de nombreuses applications, sous forme de systèmes enfouis. Ces applications sont parfois critiques, dans la mesure où toute défaillance du système informatique peut avoir des conséquences catastrophiques, tant sur le plan humain que sur le plan économique.
Nous pensons par exemple aux systèmes informatiques qui contrôlent les appareils médicaux ou certains systèmes vitaux (comme les freins) des véhicules automobiles.
Afin d’assurer la correction de ces systèmes informatiques, différentes techniques de vérification Assistée par Ordinateur ont été proposées, durant les trois dernières
décennies principalement. Ces techniques reposent sur un principe commun: donner une description formelle tant du système que de la propriété qu’il doit respecter, et appliquer une méthode automatique pour prouver que le système respecte la propriété.
Parmi les principaux modèles aptes à décrire formellement des systèmes informatiques, la classe des systèmes de transition bien structurés [ACJT96, FS01] occupe une place importante, et ce, pour deux raisons essentielles. Tout d’abord, cette classe généralise plusieurs autres classes bien étudiées et utiles de modèles à espace
d’états infini, comme les réseaux de Petri [Pet62](et leurs extensions monotones [Cia94, FGRVB06]) ou les systèmes communiquant par canaux FIFO avec pertes [AJ93]. Ensuite, des problèmes intéressants peuvent être résolus algorithmiquement sur cette classe. Parmi ces problèmes, on trouve le probléme de couverture, auquel certaines propriétés intéressantes de sûreté peuvent être réduites.
Dans la première partie de cette thèse, nous nous intéressons au problème de couverture. Jusqu’à présent, le seul algorithme général (c’est-à-dire applicable à n’importe quel système bien structuré) pour résoudre ce problème était un algorithme dit en arrière [ACJT96] car il calcule itérativement tous les états potentiellement non-sûrs et vérifie si l’état initial du système en fait partie. Nous proposons Expand, Enlarge and Check, le premier algorithme en avant pour résoudre le problème de couverture, qui calcule les états potentiellement accessibles du système et vérifie si certains d’entre eux sont non-sûrs. Cette approche est plus efficace en pratique, comme le montrent nos expériences. Nous présentons également des techniques permettant d’accroître l’efficacité de notre méthode dans le cas où nous analysons des réseaux de Petri (ou
une de leurs extensions monotones), ou bien des systèmes communiquant par canaux FIFO avec pertes. Enfin, nous nous intéressons au calcul de l’ensemble de couverture pour les réseaux de Petri, un objet mathématique permettant notamment de résoudre le problème de couverture. Nous étudions l’algorithme de Karp & Miller [KM69], une solution classique pour calculer cet ensemble. Nous montrons qu’une optimisation de cet algorithme présenté dans [Fin91] est fausse, et nous proposons une autre solution totalement neuve, et plus efficace que la solution de Karp & Miller.
Dans la seconde partie de la thèse, nous nous intéressons aux pouvoirs d’expression des systèmes bien structurés, tant en terme de mots infinis que de mots finis. Le pouvoir d’expression d’une classe de systèmes est, en quelque sorte, une mesure de la diversité des comportements que les modèles de cette classe peuvent représenter. En ce qui concerne les mots infinis, nous étudions les pouvoirs d’expression des réseaux de Petri et de deux de leurs extensions (les réseaux de Petri avec arcs non-bloquants et les réseaux de Petri avec arcs de transfert). Nous montrons qu’il existe une hiérarchie stricte entre ces différents pouvoirs d’expression. Nous obtenons également des résultats partiels concernant le pouvoir d’expression des réseaux de Petri avec arcs de réinitialisation. En ce qui concerne les mots finis, nous introduisons la classe des langages bien structurés, qui sont des langages acceptés par des systèmes de transition bien structurés étiquettés, où l’ensemble des états accepteurs est clos par le haut. Nous prouvons trois lemmes de pompage concernant ces langages. Ceux-ci nous permettent de réobtenir facilement des résultats classiques de la littérature, ainsi que plusieurs nouveaux résultats. En particulier, nous prouvons, comme dans le cas des mots infinis, qu’il existe une hiérarchie stricte entre les pouvoirs d’expression des extensions des réseaux de Petri considérées.
| Identifer | oai:union.ndltd.org:BICfB/oai:ulb.ac.be:ETDULB:ULBetd-04182007-154322 |
| Date | 20 April 2007 |
| Creators | Geeraerts, Gilles |
| Contributors | Devillers, Raymond, Van Begin, Laurent, Raskin, Jean-François, Bouajjani, Ahmed, Massart, Thierry, Boigelot, Bernard, Ouaknine, Joël |
| Publisher | Universite Libre de Bruxelles |
| Source Sets | Bibliothèque interuniversitaire de la Communauté française de Belgique |
| Language | English |
| Detected Language | French |
| Type | text |
| Format | application/pdf |
| Source | http://theses.ulb.ac.be/ETD-db/collection/available/ULBetd-04182007-154322/ |
| Rights | unrestricted, J'accepte que le texte de la thèse (ci-après l'oeuvre), sous réserve des parties couvertes par la confidentialité, soit publié dans le recueil électronique des thèses ULB. A cette fin, je donne licence à ULB : - le droit de fixer et de reproduire l'oeuvre sur support électronique : logiciel ETD/db - le droit de communiquer l'oeuvre au public Cette licence, gratuite et non exclusive, est valable pour toute la durée de la propriété littéraire et artistique, y compris ses éventuelles prolongations, et pour le monde entier. Je conserve tous les autres droits pour la reproduction et la communication de la thèse, ainsi que le droit de l'utiliser dans de futurs travaux. Je certifie avoir obtenu, conformément à la législation sur le droit d'auteur et aux exigences du droit à l'image, toutes les autorisations nécessaires à la reproduction dans ma thèse d'images, de textes, et/ou de toute oeuvre protégés par le droit d'auteur, et avoir obtenu les autorisations nécessaires à leur communication à des tiers. Au cas où un tiers est titulaire d'un droit de propriété intellectuelle sur tout ou partie de ma thèse, je certifie avoir obtenu son autorisation écrite pour l'exercice des droits mentionnés ci-dessus. |
Page generated in 0.0032 seconds