Search

This thesis is concerned with the modelling of real-time systems using Petri nets. We investigate both the problem of time representation, and of preemption (i.e., interruption of the processes of a system) which is often needed for real-time applications.We consider Petri nets without explicit temporal information. The key idea of our approach consists in introducing time through specific sub-nets representing clocks present in the system being modelled. This results in what we refer to as causal time since causality is the only means by which the precedence relationship between event occurrences is specified. For a succinct formulation of the causal time model, we use M-nets which are a class of coloured Petri nets endowed with compositional operators similar to those used by the standard process algebras. We extend the M-nets model in order to allow an efficient representation of asynchronous interprocess communication, and establish a number of theoretical results concerning such an extension. We use the resulting M-nets to model several clocks with varied characteristics, showing how they can be synchronised or kept independent. The suitability of the proposed approach is evaluated using a case study, and it is then used to give a semantics of the parallel programming language B(PN)² extended with real-time constructs.In order to deal with preemption, we propose another extension of the M-nets model supporting operators for process suspension/resuming and abortion. The resulting model is investigated at the theoretical level, and applied to B(PN)² enhanced with exceptions and tasks., Cette thèse traite de la modélisation des systèmes temps-réel à l'aidede réseaux de Petri. Nous considérons séparément la question dereprésentation du temps et celle de la préemption (interruption desprocessus d'un système) qui est d'un usage courant pour lesapplications temps-réel.Nous utilisons des réseaux de Petri sans extension par desinformations concernant le temps. Notre approche consiste alors àintroduire le temps par des sous-réseaux spécifiques représentant leshorloges du système modélisé. Le résultat est appelé tempscausal puisque seule la causalité définit la relation de précédenceentre les occurrences des événements. Afin d'obtenir une formulationélégante de l'approche causale du temps, nous utilisons le modèle desM-nets, une classe de réseaux de Petri colorés composables à lamanière des algèbres de processus. Nous étendons ce modèle de façon àpermettre la représentation efficace des communications asynchronesentre processus et les bases théoriques liées à cette extension sontrevisitées et mises à jour. Nous utilisons les M-nets ainsi étenduspour modéliser plusieurs horloges aux fonctionnalités différentes.Nous montrons comment des systèmes à plusieurs horloges, synchroniséesou non, peuvent être assez simplement obtenus. La pertinence de notreapproche est évaluée par une étude de cas et appliquée à la sémantiqued'une extension d'un langage de programmation parallèle, appeléB(PN)², par des instructions liées au temps.Pour introduire la préemption nous proposons une nouvelle extensiondes M-nets avec des opérations permettant la suspension/reprise etl'avortement. Le modèle obtenu est étudié sur le plan théorique etappliqué à l'extension de la sémantique de B(PN)² par des exceptionset un système de tâches.