en fr Forbid-Allow time Petri nets – Application to the modeling and checking of real time tasks systems Réseaux de Petri temporels à inhibitions-permissions - Application à la modélisation et vérification de systèmes de Report as inadecuate




en fr Forbid-Allow time Petri nets – Application to the modeling and checking of real time tasks systems Réseaux de Petri temporels à inhibitions-permissions - Application à la modélisation et vérification de systèmes de - Download this document for free, or read online. Document in PDF available to download.

1 LAAS - Laboratoire d-analyse et d-architecture des systèmes Toulouse

Abstract : Real time systems RTS are at the core of safety critical devices : they control the devices- behavior in such a way that they remain safe with regard to an unpredictable environment. A RTS has no other choices than to adapt to its environment : its correctness depends upon its response time to the stimuli stemming from the environment. It is widely accepted that the Time Petri nets TPN formalism is adapted to the description of RTS. However, the modeling of simple systems with only a few periodic tasks scheduled according to a basic policy remains a challenge in the worst case and can be very tedious in the most favorable one. First, we put forward some limitations of TPN regarding the modeling of a wide variety of scheduling policies, coming from the fact that this formalism is not always capable to impose a given order on events whenever they happen at the same time. Moreover, RTS are usually constituted of the same recurring features, implying a compositional modeling, but TPN are not well adapted to such a compositional use. To solve those problems we propose in this Cifre thesis - in partnership with Airbus and the Laas-Cnrs - to extend the formalism with two new dual relations, the forbid and allow relations so that time constraints can be finely tuned. Then, to assess this new extension for modeling of real time systems, we define Pola, a specific language aimed at two goals : to determine a subset of RTS which can be modeled with forbid-allow time Petri nets and to provide a simple language to the real time community which, ideally, can be checked automatically. Its semantics is given by translation into forbid-allow Time Petri nets. The state space exploration tool of the Tina toolbox have been extended so that it can model check Pola descriptions.

Résumé : Les systèmes temps réel STR sont au coeur de machines souvent jugés critiques pour la sécurité : ils en contrôlent l-exécution afin que celles-ci se comportent de manière sûre dans le contexte d-un environnement dont l-évolution peut être imprévisible. Un STR n-a d-autre alternative que de s-adapter `a son environnement : sa correction dépend des temps de réponses aux stimuli de ce dernier. Il est couramment admis que le formalisme des réseaux de Petri temporels RdPT est adapté à la description des STR. Cependant, la modélisation de systèmes simples, ne possédant que quelques tâches périodiques ordonnancées de façon basique se révèle être un exercice souvent complexe. En premier lieu, la modélisation efficace d-une gamme étendue de politiques d-ordonnancements se heurte à l-incapacité des RdPT à imposer un ordre d-apparition à des évènements concurrents survenant au même instant. D-autre part, les STR ont une nette tendance à être constitués de caract éristiques récurrentes, autorisant une modélisation par composants. Or les RdPT ne sont guère adaptés à une utilisation compositionnelle un tant soit peu générale. Afin de résoudre ces deux problèmes, nous proposons dans cette thèse Cifre - en partenariat entre Airbus et le Laas-Cnrs - d-étendre les RdPT à l-aide de deux nouvelles relations, les relations d-inhibition et de permission, permettant de spécifier de manière plus fine les contraintes de temps. Afin de cerner un périmètre clair d-adéquation de cette nouvelle extension à la modélisation des systèmes temps réel, nous avons défini Pola, un langage spécifique poursuivant deux objectifs : déterminer un sous-ensemble des systèmes temps réel modélisables par les réseaux de Petri temporels à inhibitions-permissions et fournir un langage simple à la communauté temps réel dont la vérification, idéalement automatique, est assurée par construction. Sa sémantique est donnée par traduction en réseaux de Petri temporels à inhibitions-permissions. L-explorateur d-espace d-états de la boite à outils Tina a été étendu afin de permettre la vérification des descriptions Pola.

en fr

Keywords : Real time systems time Petri nets domain specific language

Mots-clés : Systemes temps reel model checking reseau de Petri temporel langage specifique a un domaine





Author: Florent Peres -

Source: https://hal.archives-ouvertes.fr/



DOWNLOAD PDF




Related documents