A Synchronous Approach to Quasi-Periodic Systems

Guillaume Baudart 1, 2, 3
2 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Résumé : Cette thèse traite de systèmes embarqués contrôlés par un ensemble de processus périodiques non synchronisés. Chaque processus est activé quasi-périodiquement, c'est-à-dire périodiquement avec une gigue bornée. Les délais de communication sont également bornés. De tels systèmes réactifs, appelés quasi-périodiques, apparaissent dès que l'on branche ensemble deux processus périodiques. Dans la littérature, ils sont parfois qualifiés de systèmes distribués temps-réels synchrones. Nous nous intéressons aux techniques de conception et d'analyse de ces systèmes qui n'imposent pas de synchronisation globale. Les langages synchrones ont été introduits pour faciliter la conception des systèmes réactifs. Ils offrent un cadre privilégié pour programmer, analyser, et vérifier des systèmes quasi-périodiques. En s'appuyant sur une approche synchrone, les contributions de cette thèse s'organisent selon trois thématiques: vérification, implémentation, et simulation des systèmes quasi-périodiques. Vérification: L'abstraction quasi-synchrone est une abstraction discrète proposée par Paul Caspi pour vérifier des propriétés de sûreté des systèmes quasi-périodiques. Nous démontrons que cette abstraction est en général incorrecte et nous donnons des conditions nécessaires et suffisantes sur le graphe de communication et les caractéristiques temps-réels de l'architecture pour assurer sa correction. Ces résultats sont ensuite généralisés aux systèmes multi-périodiques. Implémentation: Les LTTAs sont des protocoles conçus pour assurer l'exécution correcte d'une application sur un système quasi-périodique. Nous proposons d'étudier les LTTA dans un cadre synchrone unifié qui englobe l'application et les contrôleurs introduits par les protocoles. Cette approche nous permet de simplifier les protocoles existants, de proposer des versions optimisées, et de donner de nouvelles preuves de correction. Nous présentons également dans le même cadre un protocole fondé sur une synchronisation d'horloge pour comparer les performances des deux approches. Simulation: Un système quasi-périodique est un exemple de modèle faisant intervenir des caractéristiques temps-réels et des tolérances. Pour ce type de modèle non déterministe, nous proposons une simulation symbolique, inspirée des techniques de vérification des automates temporisés. Nous montrons comment compiler un modèle mêlant des composantes temps-réels non déterministes et des contrôleurs discrets en un programme discret qui manipule des ensembles de valeurs. Chaque trace du programme résultant capture un ensemble d'exécutions possibles du programme source.
Type de document :
Thèse
Embedded Systems. Ecole normale supérieure - ENS PARIS, 2017. English
Liste complète des métadonnées


https://hal.inria.fr/tel-01507595
Contributeur : Timothy Bourke <>
Soumis le : jeudi 13 avril 2017 - 13:58:24
Dernière modification le : jeudi 15 juin 2017 - 09:09:18

Licence


Copyright (Tous droits réservés)

Identifiants

  • HAL Id : tel-01507595, version 1

Collections

Citation

Guillaume Baudart. A Synchronous Approach to Quasi-Periodic Systems. Embedded Systems. Ecole normale supérieure - ENS PARIS, 2017. English. <tel-01507595>

Partager

Métriques

Consultations de
la notice

157

Téléchargements du document

93