|
\begin{vdm_al}
module Metro1
exports all
definitions
state Metro of
doors: <Open> | <Closed>
train: <Moving> | <Stopped>
inv mk_Metro(doors,train) == not (doors = <Open> and train = <Moving>)
init metro == metro = mk_Metro(<Closed>,<Stopped>)
end
operations
Accelerate: () ==> ()
Accelerate() ==
(train:= <Moving>)
pre doors = <Closed>;
Break: () ==> ()
Break() ==
(train:= <Stopped>);
Open: () ==> ()
Open() ==
(doors:= <Open>)
pre train = <Stopped>;
Close: () ==> ()
Close() ==
(doors:= <Closed>)
end Metro1
\end{vdm_al}
The following variant of Metro1 has booleans instead of enumeration types and
implicit instead of explicit functions (note that these are not executable).
\begin{vdm_al}
module Metro1a
exports all
definitions
state Metro of
doorsopen: bool
trainmoving: bool
inv mk_Metro(doorsopen,trainmoving) == not (doorsopen and trainmoving)
init metro == metro = mk_Metro(false,false)
end
operations
Accelerate()
ext wr trainmoving
rd doorsopen
pre not doorsopen
post trainmoving;
Break()
ext wr trainmoving
post not trainmoving;
Open()
ext wr doorsopen
rd trainmoving
pre not trainmoving
post doorsopen;
Close()
ext wr doorsopen
post not doorsopen
end Metro1a
\end{vdm_al}
\section{Adding the Bell Warning and Time}
There is a requirement that a bell must ring three seconds before
doors closes. The close button must remain depressed for this period.
This kind of requirement is a bit problematic to handle, but I believe
that the suggestion below works fairly well. Time is handled almost
entirely by the environment, so it is not part of the state. However,
the time when the bell goes on, i.e.\ starts ringing, is recorded in
the state. The operation Close is split into two operations, one for
depressing the close button and one for releasing it. The operations
CloseDepress and CloseRelease have current time as a parameter.
\begin{vdm_al}
module Metro2
exports all
definitions
state Metro of
doors: <Open> | <Closed>
train: <Moving> | <Stopped>
bellon: [Time] -- The bell is not ringing if bellon is nil
inv mk_Metro(doors,train,bellon) ==
not (doors = <Open> and train = <Moving>)
init metro == metro = mk_Metro(<Closed>,<Stopped>,nil)
end
types
Time = nat;
operations
Accelerate: () ==> ()
Accelerate() ==
(train:= <Moving>)
pre doors = <Open>;
Break: () ==> ()
Break() ==
(train:= <Stopped>);
Open: () ==> ()
Open() ==
(doors:= <Open>)
pre train = <Stopped>;
CloseDepressed: Time ==> ()
CloseDepressed(t) ==
(bellon:= t)
pre bellon = nil;
CloseReleased: Time ==> ()
CloseReleased(t) ==
(if t+3 >= bellon
then doors:= <Closed>
else skip;
bellon:= nil)
pre bellon <> nil
end Metro2
\end{vdm_al}
Note that my interpretation here is that the bell rings as long as the
close button is depressed and that the doors close when it is
released. Hence, I have abstracted away from the closing assistance,
but this is included in the next version.
\section{Formalizing the Requirements}
Finally I have taken a radically different approach. The idea is to
model a system scenario, or a system ``life-time''. Here
I view the system as five sequences of time intervals, denoting when
the close button is depressed, the bell is ringing, the doors are
open, the train is moving, and the closing assistance is
activated. The correct behaviour and safety requirements of the system
are defined as functions on these sequences included in the invariant
of the System datatype. Note that I have abstracted away from the
accelerate and break buttons. Perhaps more surprisingly we don't need
the open button.
However the model includes the doors closing assistance, which must be
activated when the bell has been ringing for 3 seconds.
\begin{vdm_al}
module Metro3
exports all
definitions
types
Time = real
inv t == t>0;
Interval:: start: Time
stop: Time
inv mk_Interval(s,e) == s < e;
LifeTime = seq of Interval
inv s ==
forall i in set {1,...,len s - 1} & s(i).stop < s(i+1).start;
System::
train : LifeTime -- intervals for moving
doors : LifeTime -- intervals for open
bell : LifeTime -- intervals for ringing
closebut: LifeTime -- intervals for depressed
closeassist: LifeTime -- intervals for activated
inv mk_System(train,doors,bell,closebut,closeassist) ==
NotMovingAndOpen(train,doors) and
BellOnWhenCloseBut(bell,closebut) and
CloseAssistAfter3Secs(closeassist,bell);
functions
NotMovingAndOpen: LifeTime * LifeTime -> bool
NotMovingAndOpen(train,doors) ==
forall t in seq train, d in seq doors &
not OverlappingIntervals(t,d);
CloseAssistAfter3Secs: LifeTime * LifeTime -> bool
CloseAssistAfter3Secs(closeassist,bell) ==
forall c in seq closeassist &
exists b in seq bell &
b.stop >= b.start+3 and
c.start = b.start+3;
BellOnWhenCloseBut: LifeTime * LifeTime -> bool
BellOnWhenCloseBut(bell,closebut) ==
forall b in seq bell &
exists c in seq closebut &
SubInterval(b,c)
-- Too loose, correct?
functions -- Auxiliary functions
OverlappingIntervals: Interval * Interval -> bool
OverlappingIntervals(int1,int2) ==
undefined; -- not specified yet.
SubInterval: Interval * Interval -> bool
SubInterval(int1,int2) ==
undefined; -- not specified yet.
end Metro3
\end{vdm_al}
I have left the last two functions as an exercise! You could probably
find more requirements to model here.
A lot of questions arised during the development of this last
specification, for example, when does the bell go on and off in
relation to the close assistance and the close button, does the bell
sound for longer than 3 secs while doors are closing?
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
