Symbolic simulation of dataflow synchronous programs with timers
2017 Forum on Specification and Design Languages (FDL)(2017)
摘要
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.
更多查看译文
关键词
Programming,simulation,real-time systems,formal specifications
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络