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, ENS Paris - École normale supérieure - Paris, 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.
Type de document :
Communication dans un congrès
12th Forum on Specification and Design Languages (FDL 2017), Sep 2017, Vérone, Italy. 2017, 〈http://ecsi.org/fdl/fdl-2017-advance-program〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01575621
Contributeur : Timothy Bourke <>
Soumis le : mardi 19 septembre 2017 - 16:03:06
Dernière modification le : mardi 3 octobre 2017 - 11:52:19

Fichier

final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01575621, version 2

Collections

PSL | UPMC | INRIA

Citation

Guillaume Baudart, Timothy Bourke, Marc Pouzet. Symbolic Simulation of Dataflow Synchronous Programs with Timers. 12th Forum on Specification and Design Languages (FDL 2017), Sep 2017, Vérone, Italy. 2017, 〈http://ecsi.org/fdl/fdl-2017-advance-program〉. 〈hal-01575621v2〉

Partager

Métriques

Consultations de
la notice

43

Téléchargements du document

10