Difference between revisions of "Modelling with UML-B Class and Context Diagrams - Railway Interlocking Safety Requirements"

From Event-B
Jump to navigationJump to search
imported>Colin
imported>Colin
Line 20: Line 20:
 
*[http://users.ecs.soton.ac.uk/cfs/downloads/UML_BExamples/SafetyInvariants_UML_B.zip Solution in UML-B as a Rodin tool archive]
 
*[http://users.ecs.soton.ac.uk/cfs/downloads/UML_BExamples/SafetyInvariants_UML_B.zip Solution in UML-B as a Rodin tool archive]
 
(after downloading the zip file, go to Rodin and import existing project from archive file)
 
(after downloading the zip file, go to Rodin and import existing project from archive file)
 +
 +
==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)

Revision as of 22:16, 15 July 2010

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.

Solution

(after downloading the zip file, go to Rodin and import existing project from archive file)

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)