-Pomset pour la modélisation et la vérification de systèmes parallèles
Un comportement distribué peut être décrit avec un multi-ensemble partiellement ordonné (pomset). Bien que compacts et très intuitifs, ces modèles sont difficiles à vérifier. La principale technique utilisée dans cette thèse est de ramener les problèmes de décision de la logique MSO sur les pomsets...
Tallennettuna:
| Päätekijä: | |
|---|---|
| Muut tekijät: | , , , , , , |
| Aineistotyyppi: | Thèse numérique |
| Kieli: | Français |
| Julkaistu: |
2014.
|
| Aiheet: | |
| Linkit: | Accès au texte intégral https://theses.univ-orleans.fr/public/2014ORLE2068_vm.pdf http://www.theses.fr/2014ORLE2068/abes https://theses.hal.science/tel-01298527 |
| Huomautus: |
Thèse soutenue en co-tutelle Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) Autre(s) contribution(s) : Frédéric Loulergue (Président du jury) ; Jean-Michel Couvreur, Hamet Seydi, Frédéric Loulergue, Serge Haddad, Gane Samb Lô, Alain Griffault, Denis Poitrenaud (Membre(s) du jury) ; Serge Haddad, Gane Samb Lô (Rapporteur(s)) |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | -Pomset for modelling and verifying parallel systems |
| LEADER | 05372nam a22005057a 4500 | ||
|---|---|---|---|
| 001 | 590338 | ||
| 008 | 160504s2014 xxe ||| |||| 00| 0 fre d | ||
| 009 | PPN192982508 | ||
| 041 | 0 | |a fre |b fre |b eng | |
| 082 | |a 004.3 | ||
| 084 | |a 004 | ||
| 100 | 1 | |a Sakho, Mouhamadou Tafsir, |d 1981- | |
| 240 | 1 | 0 | |a -Pomset for modelling and verifying parallel systems |
| 245 | 1 | 0 | |a -Pomset pour la modélisation et la vérification de systèmes parallèles |c Mouhamadou Tafsir Sakho ; sous la direction de Jean-Michel Couvreur et de Hamet Seydi. |
| 256 | |a Données textuelles | ||
| 260 | |c 2014. | ||
| 500 | |a Thèse soutenue en co-tutelle | ||
| 500 | |a Titre provenant de l'écran-titre | ||
| 500 | |a Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) | ||
| 500 | |a Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) | ||
| 500 | |a Autre(s) contribution(s) : Frédéric Loulergue (Président du jury) ; Jean-Michel Couvreur, Hamet Seydi, Frédéric Loulergue, Serge Haddad, Gane Samb Lô, Alain Griffault, Denis Poitrenaud (Membre(s) du jury) ; Serge Haddad, Gane Samb Lô (Rapporteur(s)) | ||
| 502 | |a Thèse de doctorat. Mathématiques-Informatique. Orléans. 2014 | ||
| 502 | |a Thèse de doctorat. Mathématiques-Informatique. Université polytechnique de l'Ouest Africain (Dakar, Sénégal). 2014 | ||
| 520 | |a Un comportement distribué peut être décrit avec un multi-ensemble partiellement ordonné (pomset). Bien que compacts et très intuitifs, ces modèles sont difficiles à vérifier. La principale technique utilisée dans cette thèse est de ramener les problèmes de décision de la logique MSO sur les pomsets à des problèmes de décision sur les mots. Les problèmes considérés sont la satisfiabilité et la vérification. Le problème de la vérification pour une formule donnée et un pomset consiste à décider si une interprétation est vraie, et le problème de satisfiabilité consiste à décider si un pomset répondant à la formule existe. Le problème de satisfiabilité de MSO sur pomsets est indécidable. Une procédure de semi-décision peut apporter des solutions pour de nombreux cas, en dépit du fait qu'elle peut ne pas terminer. Nous proposons un nouveau modèle, que l'on appelle -Pomset, pouvant rendre l'exploration des pomsets possible. Par conséquent, si une formule est satisfiable alors notre approche mènera éventuellement à la détection d'une solution. De plus, en utilisant les -Pomsets comme modèles pour systèmes concurrents, le model-checking de formules ordre partiel sur systèmes concurrents est décidable. Certaines expérimentations ont été faites en utilisant l'outil MONA. Nous avons comparé aussi la puissance expressive de certains modèles classiques de la concurrence comme les traces de Mazurkiewicz avec les -Pomsets. | ||
| 520 | |a Multiset of partially ordered events (pomset) can describe distributed behavior. Although very intuitive and compact, these models are difficult to verify. The main technique used in this thesis is to bring back decision problems for MSO over pomsets to problems for MSO over words. The problems considered are satisfiability and verification. The verification problem for a formula and a given pomset consists in deciding whether such an interpretation exists, and the satisfiability problem consists in deciding whether a pomset satisfying the formula exists. The satisfiability problem of MSO over pomsets is undecidable. A semi-decision procedures can provide solutions for many cases despite the fact that they may not terminate. We propose a new model, so called -Pomset, making the exploration of pomsets space possible. Consequently, if a formula is satisfiable then our approach will eventually lead to the detection of a solution. Moreover, using -Pomsets as models for concurrent systems, the model checking of partial order formulas on concurrent systems is decidable. Some experiments have been made using MONA. We compare also the expressive power of some classical model of concurrency such as Mazurkiewicz traces with our -Pomsets. | ||
| 538 | |a Configuration requise : un logiciel capable de lire un fichier au format : PDF | ||
| 650 | |a Parallélisme (informatique) | ||
| 650 | |a Traitement réparti | ||
| 650 | |a Ensembles partiellement ordonnés | ||
| 650 | |a Logiciels |x Vérification | ||
| 650 | |a Théorie des traces | ||
| 650 | |a Thèses et écrits académiques | ||
| 700 | 1 | |a Couvreur, Jean-Michel, |d 1959- |4 ths |4 opn | |
| 700 | 1 | |a Seydi, Hamet. |4 ths |4 opn | |
| 700 | 1 | |a Loulergue, Frédéric, |d 1973- |4 opn | |
| 700 | 1 | |a Haddad, Serge, |d 1956- |4 opn | |
| 700 | 1 | |a Lô, Gane Samb, |d 1958- |4 opn | |
| 700 | 1 | |a Griffault, Alain, |d 1960- |4 opn | |
| 700 | 1 | |a Poitrenaud, Denis, |d 1964- |4 opn | |
| 710 | 2 | |a Université d'Orléans. |4 dgg | |
| 856 | 4 | |q PDF |s 1494148 |u http://www.theses.fr/2014ORLE2068/document |z Accès au texte intégral | |
| 856 | 4 | |u https://theses.univ-orleans.fr/public/2014ORLE2068_vm.pdf | |
| 856 | 4 | |u http://www.theses.fr/2014ORLE2068/abes | |
| 856 | 4 | |u https://theses.hal.science/tel-01298527 | |
| 997 | |0 590338 |1 Thèse numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||