Symbolic Simulation of Dataflow Synchronous Programs with Timers

Guillaume Baudart 1 Timothy Bourke 2, 3 Marc Pouzet 2, 3, 4
3 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.
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 [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01575621
Contributeur : Timothy Bourke <>
Soumis le : vendredi 1 décembre 2017 - 17:13:49
Dernière modification le : samedi 12 janvier 2019 - 01:22:54

Fichier

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

Identifiants

  • HAL Id : hal-01575621, version 3

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-01575621v3〉

Partager

Métriques

Consultations de la notice

333

Téléchargements de fichiers

60