Cette thèse traite de la modélisation des systèmes temps-réel à l'aide<br />de réseaux de Petri. Nous considérons séparément la question de<br />représentation du temps et celle de la préemption (interruption des<br />processus d'un système) qui est d'un usage courant pour les<br />applications temps-réel.<br /><br />Nous utilisons des réseaux de Petri sans extension par des<br />informations concernant le temps. Notre approche consiste alors à<br />introduire le temps par des sous-réseaux spécifiques représentant les<br />horloges du système modélisé. Le résultat est appelé temps<br />causal puisque seule la causalité définit la relation de précédence<br />entre les occurrences des événements. Afin d'obtenir une formulation<br />élégante de l'approche causale du temps, nous utilisons le modèle des<br />M-nets, une classe de réseaux de Petri colorés composables à la<br />manière des algèbres de processus. Nous étendons ce modèle de façon à<br />permettre la représentation efficace des communications asynchrones<br />entre processus et les bases théoriques liées à cette extension sont<br />revisitées et mises à jour. Nous utilisons les M-nets ainsi étendus<br />pour modéliser plusieurs horloges aux fonctionnalités différentes.<br />Nous montrons comment des systèmes à plusieurs horloges, synchronisées<br />ou non, peuvent être assez simplement obtenus. La pertinence de notre<br />approche est évaluée par une étude de cas et appliquée à la sémantique<br />d'une extension d'un langage de programmation parallèle, appelé<br />B(PN)², par des instructions liées au temps.<br /><br />Pour introduire la préemption nous proposons une nouvelle extension<br />des M-nets avec des opérations permettant la suspension/reprise et<br />l'avortement. Le modèle obtenu est étudié sur le plan théorique et<br />appliqué à l'extension de la sémantique de B(PN)² par des exceptions<br />et un système de tâches.
Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00114680 |
Date | 20 June 2002 |
Creators | Pommereau, Franck |
Source Sets | CCSD theses-EN-ligne, France |
Language | French |
Detected Language | French |
Type | PhD thesis |
Page generated in 0.0016 seconds