Symbolic Simulation of Dataflow Synchronous Programs with Timers

Guillaume Baudart 1 Timothy Bourke 2, 3, 4 Marc Pouzet 2, 3, 4, 5
4 Parkas - Parallélisme de Kahn Synchrone
Inria de Paris, DI-ENS - Département d'informatique de l'École normale supérieure, CNRS - Centre National de la Recherche Scientifique
Abstract : The synchronous language Lustre and its descendants have long been used to program and model discrete controllers. Recent work shows how to mix discrete and continuous elements in a Lustre-like language called Zélus. The resulting hybrid programs are deterministic and can be simulated with a numerical solver. In this article, we focus on a subset of hybrid programs where continuous behaviors are expressed using timers, nondeterministic guards, and invariants, as in Timed Safety Automata. We propose a source-to-source compilation pass to generate discrete code that, coupled with standard operations on Difference-Bound Matrices, produces symbolic traces that each represent a set of concrete traces.
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download
Contributor : Timothy Bourke <>
Submitted on : Tuesday, September 19, 2017 - 4:03:06 PM
Last modification on : Tuesday, April 24, 2018 - 5:20:15 PM


Files produced by the author(s)


  • HAL Id : hal-01575621, version 2


Guillaume Baudart, Timothy Bourke, Marc Pouzet. Symbolic Simulation of Dataflow Synchronous Programs with Timers. 12th Forum on Specification and Design Languages (FDL 2017), Electronic Chips & System Design Initiative (ECSI), Sep 2017, Vérone, Italy. ⟨hal-01575621v2⟩



Record views


Files downloads