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: