Séminaire
Vendredi 9 octobre 1998 - 14h00
Salle de conférences Michel Métivier
Il est reconnu qu'il n'existe pas de méthodologie générale
pour écrire des spécifications temporisées correctes. En effet, les
systèmes temporisés
différent des systèmes non temporisés du fait que leurs
séquences d'exécution sont composées de phases alterneés d'exécution
d'actions de durée zéro et de progression du temps.
Lorsque l'on décrit un système comme la composition
parallèle de composantes temporisées indépendantes, il n'est pas en
général facile
de préserver cette propriété, étant donné que le temps doit progresser
de façon
synchrone dans toutes les composantes. Nous avons démontré qu'une source
de problèmes
dans les formalismes existants est le fait que les opérateurs de mise en
parallèle
composent indépendamment les actions et les pas temporisés.
Nous définissons un cadre général pour la composition des systèmes
temporisés
représentés par des automates temporisés. Ce modèle est une extension
des automates
par des variables continues, appelées horloges, qui mesurent
le temps écoulé depuis leur dernière initialisation.
Les horloges peuvent être testées et modifiées
aux transitions qui sont de durée nulle. Deux types de prédicats sont
associés aux transitions : des gardes qui déterminent quand elles peuvent
être exécutées et des dates limites qui caractérisent les états
d'urgence.
Nous proposons un cadre général pour la composition d'automates
temporisés qui distingue
différents types de synchronisation des transitions. Ces derniers
correspondent
à des opérations de composition des gardes et des dates limites des
transitions
synchronisées. Les opérations de composition préservent l'absence de
blocage local
et garantissent la propriété de "progrès maximal".
Ces résultats permettent également une unification des différents
formalismes
de description des systèmes temporisés et tels que des automates
temporisés, des algèbres de processus temporisés
et des réseaux de Petri temporisés.
| Page d'accueil Irisa | Manifestations
scientifiques | Comment se rendre
à l'Irisa ? |
webmaster@irisa.fr, juillet 1998