Back in the day of mechanical signalling, it was comparatively simple to prove that signalling interlockings did what they were supposed to do. There were drawings to study and a finished mechanical system that could be tested. The interlockings themselves were fairly limited in their application, perhaps covering one junction or, at most, a series of junctions such as at a station throat, but it was all fairly comprehensible.
Then along came computer systems. Suddenly, the problem was immeasurably more complex. Every line of code could alter how the system worked and interlockings grew to control larger areas, introducing possibilities of more interactions. So how to check it? With teams of computer experts who were also signalling engineers, or signalling engineers who were also computer programmers, laboriously going through the program line by line?
A sensible and standardised approach was needed. So-called ‘Formal Methods’ are mathematical techniques used to specify, develop and verify computer programs and systems. They seemed like obvious candidates, but would have to be modified to work on safety-critical signalling systems.
Railway Industry Association Standard 23, (RIA 23) was developed back in the very early 1990s. ‘Formal Proof of Program’ was one of the selected techniques, labelled R for ‘recommended’ (as opposed to HR – ‘Highly Recommended’), for all (Safety Integrity Level) SIL 3 and SIL 4 systems. It was the forerunner to IEC (International Electrotechnical Commission) standard SC65A, concerned with the functional safety of electrical/electronic/programmable electronic systems (which would encompass safety-related software), and the BS EN 50128 standard – Railway applications, communication, signalling and processing systems, software for railway control and protection systems.
The standard has evolved such that formal methods seen today recommend ‘R’ for SIL 1 and 2, and ‘HR’ for SIL 3 and 4. Clearly progress has been made with the standards.
However, there are many preconceptions on what ‘formal methods’ means. One of the more common definitions is ‘Using mathematically rigorous techniques and tools for the specification, design and verification of software and hardware systems’. In the early 1990s, few formal methods existed, with VDM (Vienna Development Method) and the use of Z-notation being two of the options available at the time.
There was good reason for the early standards to only ‘recommend’ formal methods, as they were very much in the early stages of evolution. Not only were they the preserve of academia, but also they were certainly not sufficiently mature to allow industry adoption. Most such methods lacked support for automatic formal proof. It has been a long journey to bring them to the level of sophistication that is available today.
First foray
In 2001, Siemens Rail Automation (which at that time was Invensys Rail) worked with the National Physical Laboratory (NPL) – the distributor of products from Prover Technology in the UK – on formal proof of requirements against an interlocking. In those early days, the safety requirements (the signalling principles) were the preserve of experienced ‘Signalling Engineers’. Written requirements, as we understand and use them today, just did not exist at the time.
This was a major first hurdle. What were thought to be ‘clear requirements’ were, in fact, imprecise. The combination of a lack of understanding of the necessity for precise requirements and the toolset itself caused considerable challenges. The approach was not considered viable for commercial use at the time.
Second foray
Several years later, as a result of a technology change with the Trackguard Westrace Mk I interlocking (configured by means of ladder logic) being replaced by the Mk II interlocking that is in use today, the capacity for configuration data increased ten-fold. With the higher potential for error as a result of increased data capacity, and the opportunity to apply the new technology onto Network Rail infrastructure through modular signalling, both templated design methods and formal methods approaches were investigated.
By this time, the understanding of the necessity for precise requirements had matured and, compared to the early days of the project, tool support had evolved considerably and established a long track record in railway signalling application.
Prover Technology’s standard process for development and Validation & Verification (V&V) of interlocking system software, Prover Trident, is based on using a generic requirement specification library for a particular railway. This library is defined in the PiSPEC language and includes design, test and safety requirements.
Based on the library, the software tool suite Prover iLock™ provides configuration and automatic generation of interlocking data, including simulation and verification and all test cases and safety requirements for the particular location.
Prover Certifier™ is a sign-off verification tool developed in compliance with SIL 4, creating the safety evidence for the location, based on automated formal proof.
Clearly, using a formal approach such as this requires a definition of both the safety strategy and the approach, to gain acceptance with the customer and, internally, with the design and test community.
By this time, the process had evolved from just using formal proof to also including the generation of the data, test of the data and sign-off verification – in other words, complete automation of the process from a data configuration perspective.
The architecture of the system comprises a suite of generic specifications, including the generic rules (design, test and safety), which have a 1:1 relationship with the ‘Signalling Rules’ for a specific infrastructure owner and are only specified once.
Once completed, the next step in the process is the specification of the specific installation, in other words the Scheme Plan. This is either entered in XML (extensible markup language) format, electronically via SDEF (standard data exchange format) as specified by Network Rail, or using other electronic formats, for instance RailML (European open data exchange format).
Once these are in place, the other manual input to the process is defining the input/output mapping that specifies the allocation of function names to mnemonics.
Results of the second foray
Data for the Shrewsbury to Crewe (SYC) Modular Signalling project for Network Rail was prototyped as a single interlocking (today there are three interlockings). A number of iterations of the evolvement of the ‘Safety Requirements’ occurred between Siemens and Prover engineers (configurers of the toolset) but, in concept, the whole process created the interlocking code, test cases, safety requirements and verified and simulated the application in less than 40 minutes once set up. This demonstrated not only the viability of the toolset, but also that any future changes to the layout or signalling principles could be easily changed and rerun in minutes.
Whilst the process of generation and test had been proven by the prototype SYC installation, clearly the safety argument for the tool use was significantly more of a challenge. The basic premise used for the auto-generation and auto-test of the configured data is for a suite of SIL0 applications which, once complete, are presented to the existing Westrace Graphical Configuration System (GCS) toolset (in the same manner as would be used with templates). The application data is then subject to consistency checking, compilation, de-compilation and reverse checking, prior to input to Prover Certifier for sign-off verification.
This process was subject to independent assessment by Professor John McDermid of the University of York, who concluded: “Siemens is to be commended for the strategy it has followed in introducing formal methods into its processes. Formal methods do offer benefits, but they are not a panacea and the approach adopted by Siemens seems to be balanced and to have due attention to the need to demonstrate the integrity of tools on which the process relies, and also to acknowledge the important role of humans in the process.”
Third foray
Subsequently, an opportunity arose to apply Prover Technology to an overseas metro contract. In essence, this encompassed the implementation of the sign-off verification (certification) process only, with the configuration data having already been generated and tested using conventional means. This required a slightly different approach, whilst the definition and review of the safety requirements remained one of the major activities.
The input of the geographical representation of the railway was a minor challenge (this project entered the geographical representation manually). After the third iteration of conventional testing, the forth iteration was tested solely with the toolset.
Lessons learned
The biggest problems faced on any project are imprecise, ambiguous or conflicting requirements. During development of the generic application, requirements need to be presented in natural language so they can easily be translated into the toolset code. This removes ambiguity and forces conflicting requirements to be expanded to a more explicit form so the conflict can be removed. As signalling engineers tend to talk in a language that software engineers don’t understand, this process can be harder than it sounds!
The safety requirements, themselves based upon two previously and successfully implemented projects, still contained some requirements that were imprecise, ambiguous or conflicting. While sufficient for conventional development that relies on principles testers’ knowledge, imprecise requirements raise exceptions when the toolset is run. So, preciseness of requirements is key to successful deployment.
Having a baseline of design, safety and testing requirements for the generic application agreed at the start of the project helps avoid scope creep and minimises changes during the project lifecycle.
The downside to this reliance on the generic application is that getting a project off the ground is labour intensive.
Any missed safety requirements limit the scope of the safety verification.
With a tool-assisted process for development and V&V, much of the V&V and manual steps are automated. This moves the focus to capturing the requirements – traditional V&V has used more ad-hoc verification of interlocking data, not requiring the same level of requirement capture. Therefore, the design, review and checking process of generic application specifications has to be extremely robust.
The tools for formal proof analyse the interlocking logic by only looking at the critical functions defined in the object model, determining whether safety requirements can be broken or not. This is a more economical way of data verification and avoids the complications caused by irrelevant warnings.
Principles testers have a habit of trying to test every contact in a ladder logic rung, resulting in lots of test logs which either question the design or state that they are unable to verify the design due to it being untestable. Using formal proof analysis, the logic can be scrutinised in greater detail, and each safety requirement can be determined to either hold or have a counter example. For example, there have been examples where safety requirements are not met for individual cycles, which is very hard to establish using traditional testing methods.
One of the issues was determining what additional testing evidence was required, over and above the level of verification that was automated by the Prover toolset. This was essential to the process of developing the safety principles, and resulted in a further iteration of the toolset. When the model was initially developed, the primary focus was on the ‘Signalling Principles’, the operation of the overall system and its verification wasn’t fully taken into account.
Overall, this foray has been successful, allowing for future modifications to be verified solely using Prover Certifier and replacing current principles testing for data.
Object models
In parallel to the above, significant work has been undertaken capturing requirements contained within Network Rail’s Modular Signalling Handbook. As previously noted, missing, ambiguous or implied (badly specified) signalling requirements will lead to incomplete specification and thus incomplete proof. So, the importance of requirements capture cannot be emphasised strongly enough.
This led to a comprehensive trawl of, not only the UK Modular Signalling Handbook, but also other existing standards within the Network Rail portfolio (there is significant fragmentation on this subject, and many different documents), to produce a comprehensive object model – one which splits basic interlocking functionality into ‘objects’.
The object model is a central part of the generic application, used within the generic safety specification, generic design specification and generic test specification. Apart from the objects themselves, the object model defines attributes of each object and the relationships to other objects within the model.
The diagram shows an object model – a representation of the characteristics of an auto signal and its relationship and multiplicity with signalling objects. The properties (relationships, static and dynamic attributes) of abstract objects are inherited by their offspring objects, with generic properties defined at the highest possible level in the inheritance tree to avoid repetition.
Adding the definition of the inputs, outputs, dynamic and static attributes (name, control bits and function), the model of the auto signal becomes complete. With all objects modelled, the overall object model can be used to define the design and safety properties for all modular signalling applications.
This was clearly a complex and time-consuming task, with traceability to the existing standards in place and formal review with signalling experts, but did give high confidence of completeness and correctness.
The next task is the derivation of the safety requirements which, based on the natural language requirements and the object model, are defined in terms of the object model to become the ‘formal’ generic safety specification. In combination with the generic design specification, the document that defines the ‘design’ rules, and the generic test specification, the document that defines the ‘test’ rules, these form the ‘Generic’ suite of ‘Requirements’ that input into the toolset.
Prover Certifier is now being implemented in parallel to the traditional well-tried and tested method of creation and test of a specific modular interlocking to be commissioned in the UK. The next step – Generic Use for Modular Signalling?
International implementation
A number of railway infrastructure managers (IMs) today have contract requirements that mandate the use of formal proof for safety verification, prior to commissioning of interlocking and CBTC systems. Examples include Trafikverket in Sweden, RATP on Paris Metro, New York City Transit and Stockholm Metro. There is reason to believe that many other IMs will follow suit as they increasingly demand reduced engineering effort and duration for system delivery – the use of automation tools and sign-off verification of IM requirements are key ingredients to be able to meet this demand.
From a technology point of view, the obstacles are few, if any. The major challenge lies with people and mind-sets. One way to approach this is by the gradual introduction of new tools and processes in production projects, gaining the trust of and educating the signalling engineering experts and IMs involved.
For some, it may be just as well to skip the gradual introduction and directly replace existing processes with automated development and sign-off verification. This is the approach taken by the Class 1 freight railroad Canadian Pacific in North America – there were clear business benefits in introducing automated development with Prover iLock, based on a generic application defining signalling principles.
There are several other examples where such full automation processes are in use in Europe, including at Stockholm Metro.
Assured future
It is clear that the ‘Formal Methods’ seen in the early 1990s have evolved significantly. Formal proof as a means to verify safety has matured to the point that it can be applied for any railway interlocking system. Proof of safety can also be used within automated development processes for railway interlockings.
Siemens has worked in partnership with Prover Technology to demonstrate the worth of these tools in terms of feasibility on both UK infrastructure (generation and test of configuration data on Shrewsbury-Crewe in 40 minutes) and non-UK infrastructure (formal proof only).
There remain many hearts and minds to win over and the journey requires a considerable change in behaviours within the signalling industry. It is more than a concept, there are other signalling suppliers taking this approach, and there are other providers of Formal Methods toolsets on the market, but the tools and processes are here to stay.
This article was written by Pete Duggan, chief engineer at Siemens Rail Automation
