//img.uscri.be/pth/a616ebb13833007feee14e63ed3f451e1365f4a1
Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

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

De
203 pages
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
Voir plus Voir moins

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.3.2 Langages synchrones 23
2.3.3 Flot de données synchrones 24
2.3.4 Suivi d’occurrences 25
2.3.5 Base de données temps réel 26
2.4 Approches dirigées par les modèles 26
2.4.1 UML 26
2.4.2 AADL 27
2.5 Les systèmes de transitions 28
2.5.1 Introduction 28
2.5.2 Algèbres de processus 31
2.5.3 Automates Temporisés 32
2.5.4 Réseaux de Petri temporisés 35
2.5.5 Le langage TLA (Temporal Logic of Actions) 37
2.6 Conclusion 37
3 O U T I L S P O U R L A S P É C I FI C AT I O N D ’ U N S Y S T È M E 39
3.1 Définitions préliminaires 39
3.1.1 Introduction du temps 39
3.1.2 Les horloges 41
3.2 La relation d’observation 42
3.2.1 Définition 42
3.2.2 Restriction de la relation d’observation 43
3.2.3 Architecture d’un système 45
3.2.4 Horloges d’une observation 45
3.2.5 Sémantique opérationnelle de la relation d’observation 47
3.3 Outils pour définir les propriétés temps réel d’un système 48
3.3.1 Profil temporel d’une variable 48
3.3.2 Occurrences 53
3.3.3 Chemins de propagation 58
3.4 Récapitulatif 64
4 S P É C I FI C AT I O N D’ U N S Y S T È M E PA R L’ O B S E RVAT I O N 67
4.1 Comportement temporel d’une variable 67
94.2 Propriétés sur la propagation des occurrences 68
4.2.1 Forme générale 68
4.2.2 Propriétés temps réel d’un chemin 69
4.2.3 Différences et complémentarité des différents propriétés 73
4.2.4 Quelques résultats 74
4.2.5 Influence des propriétés des différents chemins 79
4.3 Spécification d’un système 79
4.3.1 Définition d’une spécification 79
4.3.2 Caractéristiques d’une spécification 80
5 R É G I M E I N I T I A L 83
5.1 Introduction du problème et de sa solution 83
5.2 Redéfinition des propriétés d’une spécification 85
5.2.1 Régime initial d’une variable 85
5.2.2 d’un chemin de propagation 86
5.2.3 Régime initial d’une spécification 87
5.3 Choix du temps de sortie des régimes initiaux 88
5.3.1 Choix du temps de sortie du régime initial d’une variable 88
5.3.2 du de sortie du d’un chemin 89
5.4 Sortie du régime initial d’une spécification en temps borné 91
5.4.1 Définitions préliminaires 91
5.4.2 Calcul du temps de sortie du régime initial 95
6 S Y S T È M E D E T R A N S I T I O N S D É FI N I PA R U N E S P É C I FI C AT I O N 101
6.1 Introduction 101
6.1.1 Satisfiabilité d’une spécification 101
6.1.2 Architecture étudiée 102
6.1.3 Différence entre la et un système de transitions 102
6.1.4 Action associée à une variable 103
6.2 Reformulation des propriétés d’une spécification 103
6.2.1 Sporadicité et périodicité 104
6.2.2 Propriétés sur la propagation des occurrences 112
6.3 Variables auxiliaires 121
6.3.1 Historique des occurrences 121
6.3.2 Conditions d’anticipation 129
6.4 Système de transitions équivalent à une spécification 130
6.4.1 Action associée à une variable 130
6.4.2 État initial 133
6.4.3 Système de transitions équivalent à une spécification 133
7 É Q U I VA L E N C E À U N S Y S T È M E FI N I 139
7.1 Introduction du problème et de sa solution 139
7.1.1 Introduction 139
7.1.2 Définition de la relation d’équivalence 139
7.1.3 Choix de l’intervalle d’analyse 142
7.2 Système de transitions fini équivalent à une spécification 145
7.2.1 Relation de transition 145
7.2.2 Action associée à une variable 146
7.2.3 Propriétés 148
7.2.4 Équivalence des systèmes de transitions 155
7.2.5 Complexité du système de réduit 160
8 E X E M P L E D E S P É C I FI C AT I O N 163
10