Symbolic Simulation of Dataflow Synchronous Programs with Timers

Guillaume Baudart 1 Timothy Bourke 2, 3 Marc Pouzet 2, 3, 4
3 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 : 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

https://hal.inria.fr/hal-01575621
Contributor : Timothy Bourke <>
Submitted on : Friday, December 1, 2017 - 5:13:49 PM
Last modification on : Saturday, January 12, 2019 - 1:22:54 AM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01575621, version 3

Citation

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-01575621v3⟩

Share

Metrics

Record views

368

Files downloads

96