A Synchronous Approach to
Quasi-Periodic Systems
Guillaume Baudart's PhD Thesis
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 are connected together. In the distributed systems literature they are also known as synchronous real-time models. We focus on techniques for the design and analysis of such systems without imposing a global clock 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 abstraction is not sound in general and give necessary and sufficient conditions on 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.
Source Code
The source code presented throughout the thesis is available on GitHub.
| Dependency | Version | Reason |
|---|---|---|
| Zélus | Required == 1.2.3 | Compile the examples to OCaml code |
| OCaml | Required == 4.04.0 | Run the Zélus compiler and compile the examples |
| XQuartz | Optional >= 2.7.9 | Required on MacOS to run the examples using OCaml Graphics |
Related Publications
- Soundness of the Quasi-Synchronous Abstraction,
with Timothy Bourke and Marc Pouzet
International Conference on Formal Methods in Computer-Aided Design (FMCAD), Oct. 2016
[ bibtex | paper ]We show that the 'quasi-synchronous' abstraction is not sound for general systems of more than two processes and propose necessary and sufficient conditions to recover soundness.
Many critical real-time embedded systems are implemented as a set of processes that execute periodically with bounded jitter and communicate with bounded transmission delay. The 'quasi-synchronous' abstraction was introduced by P. Caspi for model-checking the safety properties of applications running on such systems. The simplicity of the abstraction is appealing: the only events are process activations; logical steps account for transmission delays; and no process may be activated more than twice between two successive activations of any other.
We formalize the relation between the real-time model and the quasi-synchronous abstraction by introducing the notion of a unitary discretization. Even though the abstraction has been applied several times in the literature, we show, surprisingly, that it is not sound for general systems of more than two processes. Our central result is to propose necessary and sufficient conditions on both communication topologies and timing parameters to recover soundness.
- Loosely Time-Triggered Architectures: Improvements and Comparisons,
with Albert Benveniste and Timothy Bourke
International Conference on Embedded Software (EMSOFT), Oct. 2015. Best paper nominee
[ bibtex | paper ]An LTTA is the combinaison of a Quasi-Periodic architecture with a protocol for deploying synchronous applications. We present two protocols in a synchronous framework and compare this approach to Clock-Synchronization.
Loosely Time-Triggered Architectures (LTTAs) are a proposal for constructing distributed embedded control systems. They build on the quasi-periodic architecture, where computing units execute 'almost periodically', by adding a thin layer of middleware that facilitates the implementation of synchronous applications.
We show how the deployment of a synchronous application on a quasi-periodic architecture can be modeled using a synchronous formalism. Then we detail two protocols, Back-Pressure LTTA, reminiscent of elastic circuits, and Time-Based LTTA, based on waiting. Compared to previous work, we present controller models that can be compiled for execution and a simplified version of the Time-Based protocol. We also compare the LTTA approach with architectures based on clock synchronization.
- Loosely Time-Triggered Architectures: Improvements and Comparisons,
with Albert Benveniste and Timothy Bourke
ACM Transaction on Embedded Computing Systems (TECS), Vol.15 N.4 Aug. 2016
[ bibtex | paper | website ]Journal version of the EMSOFT'15 paper on LTTAs with and overview of the Zélus language and two optimizations for systems using broadcast communication.
Loosely Time-Triggered Architectures (LTTAs) are a proposal for constructing distributed embedded control systems. They build on the quasi-periodic architecture, where computing units execute 'nearly periodically', by adding a thin layer of middleware that facilitates the implementation of synchronous applications.
In this paper, we show how the deployment of a synchronous application on a quasi-periodic architecture can be modeled using a synchronous formalism. Then we detail two protocols, Back-Pressure LTTA, reminiscent of elastic circuits, and Time-Based LTTA, based on waiting. Compared to previous work, we present controller models that can be compiled for execution, a simplified version of the Time-Based protocol and optimizations for systems using broadcast communication. We also compare the LTTA approach with architectures based on clock synchronization.
- A Unifying View of Loosely Time-Triggered Architectures,
with Albert Benveniste, Anne Bouillard and Paul Caspi
INRIA Research Report RR-8494, Mar. 2014
[ bibtex | paper ]This research report is a corrected version of a paper which appeared at EMSOFT'2010 with the same title. It presents the two LTTA protocols, Back-Pressure and Time-Based, in a single unified Petri-Net framework.
Cyber-Physical Systems require distributed architectures to support safety critical real-time control. Hermann Kopetz' Time-Triggered Architecture (TTA) has been proposed as both an architecture and a comprehensive paradigm for systems architecture, for such systems. TTA offers the programmer a logical discrete time compliant with synchronous programming, together with timing bounds. A clock synchronization protocol is required, unless the local clocks used themselves provide the recquired accuracy. To relax the strict requirements on synchronization imposed by TTA, Loosely Time-Triggered Architectures (LTTA) have been proposed. In LTTA, computation and communication units are all triggered by autonomous, unsynchronized, clocks. Communication media act as shared memories between writers and readers and communication is non blocking. This is at the price of communication artifacts (such as duplication or loss of data), which must be compensated for by using some "LTTA protocol". In this paper we pursue our previous work by providing a unified presentation of the two variants of LTTA (token- and time-based), with simplified analyses. We compare these two variants regarding performance and robustness and we provide ways to combine them.
This report was prepared for a lecture in Gérard Berry's seminar series at the Collège de France, March 5, 2014; it is a corrected version of a paper, which appeared at Emsoft'2010. It is dedicated to our close friend Paul Caspi who died in April 2012.
Music
Before my PhD, I worked on another application of the synchronous approach: designing a reactive language for mixed music, that is, music involving both live musicians and electronic sounds.
We gave a synchronous semantics to the Antescofo language, a DSL for authoring mixed music, and an alternative implementation of the sequencer based on an embedding inside a synchronous language, ReactiveML. We used this embedding to allow live coding with Antescofo.
We published the two following papers on this topic:
- A Synchronous Embedding of Antescofo, a Domain-Specific Language for Interactive Mixed
Music,
with Florent Jacquemard, Louis Mandel and Marc Pouzet
International Conference on Embedded Software (EMSOFT), Sept. 2013. Best paper nominee
[ bibtex | paper | website ]This article presents a synchronous semantics for the core of the Antescofo language, a DSL for authoring mixed music, and an alternative implementation based on an embedding inside a synchronous language, ReactiveML.
Antescofo is recently developed software for musical score following and mixed music: it automatically, and in real-time, synchronizes electronic instruments with a musician playing on a classical instrument. Therefore, it faces some of the same major challenges as embedded systems.
The system provides a programming language used by composers to specify musical pieces that mix interacting electronic and classical instruments. This language is developed with and for musicians and it continues to evolve according to their needs. Yet its semantics has only recently been formally defined. This paper presents a synchronous semantics for the core language of Antescofo and an alternative implementation based on an embedding inside an existing synchronous language, namely ReactiveML. The semantics reduces to a few rules, is mathematically precise and leads to an interpretor of only a few hundred lines. The efficiency of this interpretor compares well with that of the actual implementation: on all musical pieces we have tested, response times have been less than the reaction time of the human ear. Moreover, this embedding permitted the prototyping of several new programming constructs, some of which are described in this paper.
- Programming Mixed-Music in ReactiveML,
with Louis Mandel and Marc Pouzet
Workshop on Functional Art, Music, Modeling and Design (FARM), Sept. 2013
[ bibtex | paper | website ]A tutorial on how to program mixed music in ReactiveML through several examples: frère Jacques, a very simple musical round; live coding using the Antescofo library; and Steve Reich's Piano Phase.
Mixed music is about live musicians interacting with electronic parts which are controlled by a computer during the performance. It allows composers to use and combine traditional instruments with complex synthesized sounds and other electronic devices. There are several languages dedicated to the writing of mixed music scores. Among them, the Antescofo language coupled with an advanced score follower allows a composer to manage the reactive aspects of musical performances: how electronic parts interact with a musician. However these domain specific languages do not offer the expressiveness of functional programming.
We embed the Antescofo language in a reactive functional programming language, ReactiveML. This approach offers to the composer recursion, higher order, inductive types, as well as a simple way to program complex reactive behaviors thanks to the synchronous model of concurrency on which ReactiveML is built. This article presents how to program mixed music in ReactiveML through several examples.