Spécification formelle de systèmes temps réel répartis par une approche flots de données à contraintes temporelles, Formal specification of distributed real time systems using an approach based on temporally constrained data flows

Tanguy Le Berre

Description

Sous la direction de Gérard Padiou, Philippe Quéinnec
Thèse soutenue le 23 mars 2010: INPT
Une définition des systèmes temps réel est que leur correction dépend de la correction fonctionnelle mais aussi du temps d'exécution des différentes opérations. Les propriétés temps réels sont alors exprimées comme des contraintes temporelles sur les opérations du système. Nous proposons dans cette thèse un autre point de vue où la correction est définie relativement à la validité temporelle des valeurs prises par les variables du système et aux flots de données qui parcourent le système. Pour définir ces conditions de validité, nous nous intéressons au rythme de mise à jour des variables mais aussi aux liens entre les valeurs des différentes variables du système. Une relation dite d'observation est utilisée pour modéliser les communications et les calculs du système qui définissent les liens entre les variables. Un ensemble de relations d'observation modélise l'architecture et les flots de données du système en décrivant les chemins de propagation des valeurs dans le système. Les propriétés temps réels sont alors exprimées comme des contraintes sur ces chemins de propagation permettant d'assurer la validité temporelle des valeurs prises par les variables. La validité temporelle d'une valeur est définie selon la validité temporelle des valeurs des autres variables dont elle dépend et selon le décalage temporel logique ou événementiel introduit par les communications ou les calculs le long des chemins de propagation. Afin de prouver la satisfiabilité d'une spécification définie par une telle architecture et de telles propriétés, nous construisons un système de transitions à état fini bisimilaire à la spécification. L'existence de ce système fini est justifiée par des bornes sur le décalage temporel entre les variables du système. Il est alors possible d'explorer les exécutions définies par ce système de transitions afin de prouver l'existence d'exécutions infinies satisfaisant la spécification.
-Informatique
-Temps réel
-Réparti
-Vérification
-Spécification
-Formel
Real time systems are usually defined as systems where the total correctness of an operation depends not only on its logical correctness, but also on the execution time. Under this definition, time constraints are defined according to system operations. Another definition of real time systems is centered on data where the correctness of a system depends on the timed correctness of its data and of the data flows across the system. i.e. we expect the values taken by the variable to be regularly renewed and to be consistent with the environment and the other variables. I propose a modeling framework based on this later definition. This approach allows users to focus on specifying time constraints attached to data and to postpone task and communication scheduling matters. The timed requirements are not expressed as constraints on the implantation mechanism, but on the relations binding the system’s variables. These relations between data are expressed in terms of a so called observation relation which abstracts the relation between the values that are taken by some variables, the set of sources and the image. This relation abstracts the communication as well as the computational operations and a set of observation relations models the system architecture and the data flows by defining the paths along which values of sources are propagated to build the values of an image. The real time properties are expressed as constraints on the propagation paths and state the temporal validity of the values. This temporal validity is defined by the time shift between the source and the image, and specifies the propagation of timely sound values along the path to build temporally correct values of the system outputs. At this level of abstraction, the designer gives a specification of the system based on timed properties about the timeline of data such as their freshness, stability, latency etc. In order to prove the feasibility of an observation-based model, a finite state transition system bi-similar with the specification is built. The existence of a finite bi-similar system is deduced from the bounded time shift between the variables. The existence of an infinite execution in this system proves the feasibility of the specification.
-Formal spécification
-Verification
-Real time
-Distributed
-Data flow
Source: http://www.theses.fr/2010INPT0023/document

Sujets

• Informatique
• Temps réel
• Vérification
• Spécification
• Formel
• Real Time

Informations

• Publié par: Thesee
• Nombre de lectures: 37
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

THÈSE
En vue de l'obtention du
DOCTORAT DE L’UNIVERSITÉ DE TOULOUSE
Délivré par Institut National Polytechnique de Toulouse
Discipline ou spécialité In:formatique
Présentée et soutenue par Tanguy Le Berre
Le 23 mars 2010
Titre :
Spécification formelle de systèmes temps réel répartis
par une approche flots de données à contraintes temporelles
JURY
Jean-Philippe Babau (PR) - LISyC, Brest
Michel Charpentier (PR) - UNH, Durham
Mamoun Filali Amine (CR) - IRIT, Toulouse
Dominique Méry (PR) - LORIA, Nancy
Olivier Roux (PR) - IRCCyN, Nantes
Gérard Padiou (PR) - IRIT, Toulouse
Philippe Quéinnec (MC) - IRIT, Toulouse
Ecole doctorale :Mathématiques, Informatique et Télécommunications de Toulouse
Unité de recherche In:stitut de Recherche en Informatique de Toulouse
Directeur(s) de Thèse G:érard Padiou, Philippe Quéinnec
Rapporteurs : Jean-Philippe Babau, Michel Charpentier, Olivier RouxA B S T R A C T
Real time systems are usually defined as systems where the total correctness of an
operation depends not only on its logical correctness, but also on the execution time. Un-
der this definition, time constraints are defined according to system operations. Another
definition of real time systems is centered on data where the correctness of a system
depends on the timed correctness of its data and of the data flows across the system. i.e.
we expect the values taken by the variable to be regularly renewed and to be consistent
with the environment and the other variables.
I propose a modeling framework based on this later definition. This approach allows
users to focus on specifying time constraints attached to data and to postpone task
and communication scheduling matters. The timed requirements are not expressed as
constraints on the implantation mechanism, but on the relations binding the system’s
variables. These relations between data are expressed in terms of a so called observation
relation which abstracts the relation between the values that are taken by some variables,
the set of sources and the image. This relation abstracts the communication as well
as the computational operations and a set of observation relations models the system
architecture and the data flows by defining the paths along which values of sources are
propagated to build the values of an image.
The real time properties are expressed as constraints on the propagation paths and
state the temporal validity of the values. This temporal validity is defined by the time
shift between the source and the image, and specifies the propagation of timely sound
values along the path to build temporally correct values of the system outputs. At this
level of abstraction, the designer gives a specification of the based on timed
properties about the timeline of data such as their freshness, stability, latency etc.
In order to prove the feasibility of an observation-based model, a finite state transi-
tion system bi-similar with the specification is built. The existence of a finite bi-similar
system is deduced from the bounded time shift between the variables. The existence of
an infinite execution in this system proves the feasibility of the specification.
3R É S U M É
Une définition des systèmes temps réel est que leur correction dépend de la correction
fonctionnelle mais aussi du temps d’exécution des différentes opérations. Les propriétés
temps réels sont alors exprimées comme des contraintes temporelles sur les opérations
du système. Nous proposons dans cette thèse un autre point de vue où la correction
est définie relativement à la validité temporelle des valeurs prises par les variables du
système et aux flots de données qui parcourent le système.
Pour définir ces conditions de validité, nous nous intéressons au rythme de mise à
jour des variables mais aussi aux liens entre les valeurs des différentes variables du
système. Une relation dite d’observation est utilisée pour modéliser les communications
et les calculs du système qui définissent les liens entre les variables. Un ensemble de
relations d’observation modélise l’architecture et les flots de données du système en
décrivant les chemins de propagation des valeurs dans le système.
Les propriétés temps réels sont alors exprimées comme des contraintes sur ces
chemins de propagation permettant d’assurer la validité temporelle des valeurs prises
par les variables. La validité temporelle d’une valeur est définie selon la validité tem-
porelle des valeurs des autres variables dont elle dépend et selon le décalage temporel
logique ou événementiel introduit par les communications ou les calculs le long des
chemins de propagation.
Afin de prouver la satisfiabilité d’une spécification définie par une telle architecture et
de telles propriétés, nous construisons un système de transitions à état fini bisimilaire à
la spécification. L’existence de ce système fini est justifiée par des bornes sur le décalage
temporel entre les variables du système. Il est alors possible d’explorer les exécutions
définies par ce système de transitions afin de prouver l’existence d’exécutions infinies
satisfaisant la spécification.
5R E M E R C I E M E N T S
Je souhaite ici remercier les personnes qui ont contribué, directement ou indirecte-
ment, à la réalisation de ma thèse et à la rédaction de ce mémoire.
Je remercie tout d’abord les rapporteurs de mon travail, Jean-Philippe Babau, Olivier
Roux et Michel Charpentier. Je les remercie d’avoir pris le temps de lire le manuscrit,
d’avoir commenté mon travail et m’avoir conseillé. Je remercie également les membres
du jury Dominique Méry et Mamoun Filali de s’être intéressés à mon travail et d’être
venus assister à ma soutenance.
Je tiens à remercier Gérard Padiou, mon directeur de thèse, pour m’avoir accueilli en
Master de Recherche et m’avoir par la suite confié ce sujet de thèse. Malgré un emploi
du temps chargé, il m’a accompagné tout au long de ces quatre ans et m’a proposé tout
ce que l’on peut attendre d’un directeur de thèse, une oreille disponible et des conseils
avisés.
Je remercie tout particulièrement Philippe Quéinnec, mon co-directeur de thèse. C’est
véritablement une chance qu’il m’ait accompagné depuis quatre ans. Il s’est montré
disponible afin de pouvoir débattre, parfois longuement, de mon travail. Lors de ces dis-
cussions, il a su me conseiller et m’encourager tout en me laissant libre des orientations
que je voulais donner à ce travail. Sa rigueur m’a permis de corriger et perfectionner tout
ce que j’ai pu effectuer et notamment ce manuscrit. Cette thèse ne serait certainement
pas aussi aboutie s’il n’avait pas été là. Je m’excuse auprès de lui pour mes nombreuses
fautes de grammaire ou d’orthographe qu’il a corrigées depuis quatre ans.
Je souhaite remercier l’ensemble de l’équipe de recherche et d’enseignement qui m’a
accueilli et toutes les personnes que j’ai pu y côtoyer. Merci pour le cadre de travail
que vous avez proposé, merci aux permanents qui m’ont aidé dans mes activités de
recherche et d’enseignement et merci aux autres doctorants de l’équipe pour leur soutien
mutuel. Merci pour la bonne humeur dont tout le monde fait preuve.
Je remercie mon entourage, à commencer par ma famille et en particulier mes parents
qui m’ont soutenu et m’ont donné l’opportunité d’effectuer les études que je souhaitais
et donc finalement d’entreprendre cette thèse. Je remercie mes amis, à Toulouse et
ailleurs, qui ont suivi mon travail, m’ont encouragé et parfois m’ont détourné de la
thèse en me proposant les distractions et les vacances nécessaires à mon équilibre. Je
remercie finalement Perrine pour être à mes cotés en permanence, dans les bons comme
dans les mauvais moments. Il m’est impossible d’imaginer avoir conclu ce travail sans
ton support au quotidien. Merci pour tout.
Enfin, j’ai une dernière pensée pour la ville de Toulouse et le sud-ouest que je vais
quitter. Sans exagérer comme mes amis toulousains et affirmer que Toulouse est la plus
belle ville du monde, j’ai beaucoup apprécié la vie toulousaine. Ce fut un grand plaisir
d’effectuer ma thèse ici et je reviendrai toujours avec plaisir.
7TA B L E D E S M AT I È R E S
1 I N T R O D U C T I O N 13
1.1 Contexte 13
1.2 Problématique 14
1.3 Travaux de la thèse 14
1.4 Plan 15
2 A P P R O C H E S E X I S TA N T E S 17
2.1 Introduction 17
2.1.1 Systèmes temps réel 17
2.1.2 Contexte 18
2.1.3 Méthodes de vérification 19
2.1.4 Objet de l’étude 20
2.2 Logiques temporelles 21
2.3 Approches dédiées pour la spécification de systèmes temps réels 22
2.3.1 Analyse d’ordonnancement 22
2