@inproceedings{72012281dee54f308e5088f4d2c8f855,
title = "Symbolic simulation of dataflow synchronous programs with timers",
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{\'e}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 adapt a type system for mixing timers and discrete components and 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.",
keywords = "Compilation, Hybrid systems, Symbolic simulation, Synchronous languages, Timed automata, Type system",
author = "Guillaume Baudart and Timothy Bourke and Marc Pouzet",
note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2019.; Forum on specification and Design Languages Conference, FDL 2017 ; Conference date: 18-09-2017 Through 20-09-2017",
year = "2019",
month = jan,
day = "1",
doi = "10.1007/978-3-030-02215-0\_3",
language = "English",
isbn = "9783030022143",
series = "Lecture Notes in Electrical Engineering",
publisher = "Springer Verlag",
pages = "45--70",
editor = "Daniel Gro{\ss}e and Sara Vinco and Hiren Patel",
booktitle = "Languages, Design Methods, and Tools for Electronic System Design - Selected Contributions from FDL 2017",
}