Skip to Main content Skip to Navigation

A synchronous approach to quasi-periodic systems

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 metadata

Cited literature [108 references]  Display  Hide  Download
Contributor : Abes Star :  Contact
Submitted on : Thursday, June 22, 2017 - 7:05:08 PM
Last modification on : Thursday, October 29, 2020 - 3:01:42 PM
Long-term archiving on: : Wednesday, January 10, 2018 - 4:47:18 PM


Version validated by the jury (STAR)


  • HAL Id : tel-01507595, version 2



Guillaume Baudart. A synchronous approach to quasi-periodic systems. Distributed, Parallel, and Cluster Computing [cs.DC]. Université Paris sciences et lettres, 2017. English. ⟨NNT : 2017PSLEE007⟩. ⟨tel-01507595v2⟩



Record views


Files downloads