Supporting Railway Standardisation with Formal Verification

This thesis has been written in the context of the FormaSig project. This project involves a collaboration between academia and railway infrastructure managers to use formal methods to support the development of the EULYNX standard. This standard uses the SysML modelling language to define the interfaces of the various components of a signalling system (signal, point, level crossing, etcetera). The aim of the FormaSig project is to define a formal interpretation of the standard such that delivered components conforming to the standard provably satisfy a collection of safety properties. The idea is to associate with each SysML model a formal mCRL2 model. Then mCRL2’s model checker can be used to establish that the model satisfies the required safety properties, and automated model-based test technology can be used to thoroughly test compliance to the model of actual implementations. This thesis focusses on the aspects of formalisation and verification.

The first contribution is a formalisation of SysML in mCRL2. The approach taken is to generically define the structure and semantics of SysML state machines in mCRL2. This generic model forms the basis of a translation tool that encodes a set of concrete SysML models in the mCRL2 data language.

A challenge in model checking is scalability; the state space of a model tends to scale exponentially with the number of parallel components. Our second contribution is an inventory of techniques to reduce the size of the state space induced by mCRL2 models obtained through our SysML to mCRL2 translation. We found that the most effective technique for our models is compositional minimisation. With this technique the state space of the entire (monolithic) model is not computed in one go. Instead, the model is first split into components; in our case a SysML state machine is a component. The state space of each component is computed and then minimised modulo an equivalence relation. These minimised state spaces are finally combined to construct the state space of the entire model. The existing theory is extended to support branching bisimulation minimisation, greatly increasing its effectiveness.

The next contribution of this thesis is to discuss the application of the aforementioned translation and scalability techniques to several concrete EULYNX interfaces. For each interface (safety) requirements are formulated and verified using the mCRL2 toolset. The verification efforts identified errors and omissions in the standard and this led to improvements of the standard. The case studies have also led to improvements of the toolchain.

The case studies reveal that we sometimes want to verify liveness requirements stating that something good always eventually happens. For such requirements, assumptions are often needed on how events are scheduled. These range from very basic assumptions to rather strong assumptions that may not be realistic. A recently introduced notion is that of ‘justness’. In short, it is the assumption that once an action is enabled that stems from a set of parallel components then one (or more) of these components will eventually partake in an action. This seems to be a realistic assumption that is just strong enough for many liveness requirements. This thesis contributes a way to verify liveness requirements with a justness assumption for mCRL2 models. Moreover, it is applied in the aforementioned case studies.

Besides justness, the cases studies reveal another need: the concept of global variables. The semantics of mCRL2 is action-based and thus abstracts from the contents of a state; states are only distinguished by their transitions. The logic (the modal mu-calculus in the case of the mCRL2 toolset) also only refers to transitions. For models that are derived from state based formalisms (such as SysML) it can be desirable to also consider the contents of a state. For some requirements for FormaSig models we need to specify that the system always (or never) ends up in a specific SysML state. The final contribution in this thesis is a process algebra with global variables and a logic allowing references to these variables. This enables the inspection of these global variables during verification and thus allows for requirements referencing both the transitions and the contents of states. Moreover, in some settings, it allows for a more natural form of communication between parallel components (compared to message passing). The theory is applied to formulate requirements in FormaSig.