Formalized Analaysis and Verification / App. Ex. 3

ENABLE-S3 / Use Case 9 “Interlocking”: The pattern has been used to analyse a railway interlocking control system component.

The iUML-B modelling language was used. iUML-B is a plug-in for the Rodin platform and is based on Event-B.

As expected, the model was fully proved and validated. No dependability problems were discovered. Hence the analysis stages of the pattern are omitted.

Specification of Interlocking System: