Modelling with UML-B Class and Context Diagrams - Railway Interlocking Safety Requirements

From Event-B
Jump to navigationJump to search

Problem

A Railway interlocking system controls trains passing through a track layout by changing the state of Signals which can be Proceed, Warning or Stop. The signal immediately before another signal is said to be RearOf the second signal.

The track layout is divided into Routes. Each Route has an Entry signal at its start. Some Routes Conflict with others (e.g. use the same section of track). A route is locked before it is used and then unlocked again.

The following safety requirements are specified:

  • SR1 - If a signal shows Stop, the signal RearOf it must show Stop or Warning
  • SR2 - If the entry signal of a route shows Proceed or Warning, then the Route is locked
  • SR3 - If a route is locked then no route that conflicts with it is locked

Model this domain in just enough detail to be able to express the safety requirements. Use a UML-B Context diagram for the static parts and a Class Diagram for the varying parts. (Link the Classes to the ClassTypes using the Instances property of the Class).

Add invariants to your model to reflect these requirements. Add guards to your events to ensure the system does not violate the invariants. Use the prover to verify this.

Solution

Example of UML-B Class and Context Diagrams - Railway Interlocking Safety

Tips

A Class can be linked to a corresponding ClassType by setting the 'Instances' property of the Class to the ClassType.

The key combo for the 'dot' operator used in predicates and actions of a class is ,. (i.e. comma+stop)

Retrieved from ‘https://wiki.event-b.org/index.php?title=Modelling_with_UML-B_Class_and_Context_Diagrams_-_Railway_Interlocking_Safety_Requirements&oldid=6164’