Quelle metro.vdmsl Sprache: VDM

\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?

quality95%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.