|
|
Groupe OLC
Outils et Logiciels pour la
Communication
|
Projet
de
Recherche
|
Formalisation d'un croisement ferroviaire
Un exemple académique
Christophe Lohr
1 Introduction
Cet exemple décrit un contrôleur automatique qui ouvre et ferme une barrière
à un croisement de chemin de fer. Il a été présenté initialement dans
[ACHWT92]. La spécification en langage naturel reprise ici est tirée de
[KLK00].
2 Description en langage naturel
Le système correspond à la composition de trois composants : Train,
Gate, et Controller, qui s'exécutent en parallèle et se
synchronisent sur les événements : approach, leave,
lower et down.
-
Lorsqu'un train est en approche du croisement, Train envoit un
signal approach au Controller et entre dans le croisement au
moins 300 secondes plus tard. Quand un train quitte le croisement,
Train envoit un signal leave au Controller. Le signal
leave est envoyé dans les 500 secondes qui suivent le signal
approach.
- Controller envoit un signal lower à Gate
exactement 100 secondes après le signal approach et envoit un
signal raise dans les 100 secondes qui suivent exit.
- Gate répond par down au signal lower dans les
100 secondes, et répond par up au signal raise entre 100
et 200 secondes.
3 Spécification RT-LOTOS
railroad.lot
specification Railroad_Crossing : exit
type natural is boolean
sorts nat
opns + : nat,nat->nat
- : nat,nat->nat
endtype
behaviour
hide approach, leave, lower, raise, into, outto, down, up in
( Train[approach,leave,into,outto]
|[approach,leave]|
Controller[approach,lower,leave,raise] )
|[lower,raise]|
Gate[lower,raise,down,up]
where
process Train[approach,leave,into,outto] : noexit :=
approach;
( ( into; outto; leave; exit )
|[into,outto,leave]|
( ( delay(300,500) into{200}; exit )
|||
( delay(300,500) outto{200}; exit )
|||
( delay(300,500) leave{200}; exit ) ) )
>> Train[approach,leave,into,outto]
endproc
process Controller[approach,lower,leave,raise] : noexit :=
approach; delay(100) lower;
leave; latency(100) raise{100};
Controller[approach,lower,leave,raise]
endproc
process Gate[lower,raise,down,up] : noexit :=
lower; latency(100) down{100};
raise; delay(100,200) up{100};
Gate[lower,raise,down,up]
endproc
endspec
Références
- [ACHWT92]
-
R. Alur, C. Courcoubetis, N. Halbwachs, and H. Wong-Toi.
An implementation of three algorithms for timing verification based
on automata emptiness.
In 13th Real-time Systems Symposium, pages 157--166,
Phoenix, Arizona, 1992. IEEE Computer Society Press.
- [KLK00]
-
I. Kang, I. Lee, and Y.S. Kim.
An efficient state space generation for analysis of real-time
systems.
Transactions of Software Engineering, 26(5):453--477, 2000.
Retour au projet RT-LOTOS
Ce document a été traduit de LATEX par
HEVEA.