A synchronous approach to quasi-periodic systems

Guillaume Baudart 1, 2
2 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : In this thesis we study embedded controllers implemented as sets of unsynchronized periodic processes. Each process activates quasi-periodically, that is, periodically with bounded jitter, and communicates with bounded transmission delays. Such reactive systems,termed 'quasi-periodic', exist as soon as two periodic processes areconnected together. In the distributed systems literature they arealso known as synchronous real-time models. We focus on techniquesfor the design and analysis of such systems without imposing a globa lclock synchronization. Synchronous languages were introduced as domain specific languages for the design of reactive systems. They offer an ideal framework to program, analyze, and verify quasi-periodic systems. Based on a synchronous approach, this thesis makes contributions to the treatment of quasi-periodic systems along three themes: verification,implementation, and simulation.Verification: The 'quasi-synchronous abstraction' is a discrete abstraction proposed by Paul Caspi for model checking safety properties of quasi-periodic systems. We show that this abstractionis not sound in general and give necessary and sufficient conditionson both the static communication graph of the application and the real-time characteristics of the architecture to recover soundness. We then generalize these results to multirate systems.Implementation: 'Loosely time-triggered architectures' are protocols designed to ensure the correct execution of an application running on a quasi-periodic system. We propose a unified framework that encompasses both the application and the protocol controllers. This framework allows us to simplify existing protocols, propose optimized versions, and give new correctness proofs. We instantiate our framework with a protocol based on clock synchronization to compare the performance of the two approaches.Simulation: Quasi-periodic systems are but one example of timed systems involving real-time characteristics and tolerances. For such nondeterministic models, we propose a 'symbolic simulation' scheme inspired by model checking techniques for timed automata. We show how to compile a model mixing nondeterministic continuous-time and discrete-time dynamics into a discrete program manipulating sets of possible values. Each trace of the resulting program captures a set of possible executions of the source program.
Complete list of metadatas

Cited literature [108 references]  Display  Hide  Download

https://tel.archives-ouvertes.fr/tel-01507595
Contributor : Abes Star <>
Submitted on : Thursday, June 22, 2017 - 7:05:08 PM
Last modification on : Monday, January 28, 2019 - 9:03:30 AM
Long-term archiving on : Wednesday, January 10, 2018 - 4:47:18 PM

File

BAUDART2017archivage.pdf
Version validated by the jury (STAR)

Identifiers

  • 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⟩

Share

Metrics

Record views

705

Files downloads

253