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
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 : Monday, August 21, 2017 - 11:56:43 AM
Last modification on : Tuesday, April 24, 2018 - 5:20:15 PM

File

fdl2017.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01575621, version 1

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

Share

Metrics

Record views

63

Files downloads

11