Publication
FDL 2017
Conference paper

Symbolic simulation of dataflow synchronous programs with timers

View publication

Abstract

The synchronous language Lustre and its descendants have long been used to program and model discrete con-trollers. 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.

Date

Publication

FDL 2017

Authors

Share