Abstraction d'horloges
dans les systèmes synchrones flot de données - JFLA 2009
Abstract:
Les langages synchrones flot de données tels que Lustre manipulent
des séquences infinies de données comme valeurs de base. Chaque
flot est associé à une horloge qui définit les instants où la
valeur courante du flot est présente. Cette horloge est une
information de type et un système de types dédié, le calcul
d'horloges, rejette statiquement les programmes qui ne peuvent pas
être exécutés de manière synchrone. Dans les langages synchrones
existants, cela revient à se demander si deux flots ont la même
horloge et repose donc uniquement sur l'égalité d'horloges. Des
travaux récents ont montré l'intérêt d'introduire une notion
relâchée du synchronisme, où deux flots peuvent être composés dès
qu'ils peuvent être synchronisés par l'introduction d'un buffer de
taille bornée (comme c'est fait dans le modèle SDF d'Edward
Lee). Techniquement, cela consiste à remplacer le typage par du
sous-typage. Ce papier est une traduction et amélioration technique
de [1]
qui présente un moyen simple de mettre en
oeuvre ce modèle relâché par l'utilisation d'horloges abstraites.
Les valeurs abstraites représentent des ensembles d'horloges
concrètes qui ne sont pas nécessairement périodiques. Cela permet
de modéliser divers aspects des logiciels temps-réel embarqués, tels
que la gigue bornée présente dans les systèmes vidéo, le temps
d'exécution des processus temps réel et, plus généralement, la
communication à travers des buffers de taille bornée. Nous
présentons ici l'algèbre des horloges abstraites et leurs principales
propriétés théoriques.
Article : .pdf
Version longue :
.pdf
Développement
Coq :
.html,
.tgz
References
-
[1]
-
Albert Cohen, Louis Mandel, Florence Plateau, and Marc Pouzet.
Abstraction of Clocks in Synchronous Data-flow Systems.
In The Sixth ASIAN Symposium on Programming Languages and
Systems (APLAS 08), Bangalore, India, December 2008.
This document was translated from LATEX by
HEVEA.