A synchronous approach to quasi-periodic systems

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éel 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éel 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
Distributed, Parallel, and Cluster Computing [cs.DC]. PSL Research University, 2017. English. 〈NNT : 2017PSLEE007〉
Liste complète des métadonnées

Littérature citée [108 références]  Voir  Masquer  Télécharger

https://tel.archives-ouvertes.fr/tel-01507595
Contributeur : Abes Star <>
Soumis le : jeudi 22 juin 2017 - 19:05:08
Dernière modification le : mardi 12 juin 2018 - 03:48:08
Document(s) archivé(s) le : mercredi 10 janvier 2018 - 16:47:18

Fichier

BAUDART2017archivage.pdf
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-01507595, version 2

Collections

Citation

Guillaume Baudart. A synchronous approach to quasi-periodic systems. Distributed, Parallel, and Cluster Computing [cs.DC]. PSL Research University, 2017. English. 〈NNT : 2017PSLEE007〉. 〈tel-01507595v2〉

Partager

Métriques

Consultations de la notice

567

Téléchargements de fichiers

144