Rigorous verification of embedded software systems in the Rail industry
Software based systems within railway systems such as signalling and on-board systems are becoming increasingly complex. The typical approach to the development of software based systems has a cost profile heavily weighted towards the end of the project; this represents considerable project risk. For systems and software in the rail domain, IEC/EN50128 is the key system safety document whose main aim is to achieve evidence to support the safety case. Gaining the required evidence from development life cycle processes that support platform safety claims needs to be designed into all stages of the life cycle. The production of evidence should therefore drive the selection of the best development life cycle, processes and tools. The production of verification evidence through either review, analysis or test to meet IEC/EN 50128 can therefore be costly and unresponsive, even to small changes.
The use of formal methods in rail is recognised under IEC/EN50128 and is ‘Recommended’ for both architectures and software. Over the past decade, the Scandinavian countries have changed this ‘Highly Recommended’. To date, it has been assumed that experts are required to write formal specifications by hand and then to prove the necessary properties using appropriate qualified tools as support. This is not necessarily a quick or repeatable process and where in other industries formal techniques have been used, they have become company specific knowledge, not available to the wider community. Therefore in order for formal techniques to be adopted more widely in the rail industry, they need to be automated in order to achieve the required flexibility, repeatability, have a low training overhead, as well as providing evidence to support the overall platform safety case.
D-RisQ has taken an approach which enables the power of formal methods to be exploited without any specialist training. By using commonly available tools such as Simulink® and commercial autocoders it is now possible for current engineers to develop systems and software in a rigorous manner, whilst gaining as a by-product, the required evidence to support certification. The D-RisQ automated suite of tools includes Modelworks® and CLawZ® which tackle different aspects of verification. The tools can be qualified to support both development and verification and support an independence argument which strengthens the support to the platform safety case.
Modelworks® proves that requirements have been correctly captured in a design expressed in Stateflow®, or will show the manner in which compliance has failed. The design can be of a System of Systems, a single system or a software program. It allows a designer to check that the design does what is required. More importantly, it allows a proof that undesired properties will never happen, a check that is typically attempted at the end of a development life-cycle. It is also possible to show behaviour under failure conditions. Modelworks can be used to show the behaviour of highly distributed Systems-of Systems such as signalling and can be used to help the safe implementation of signalling upgrades, including the behaviour of human interaction where necessary.
CLawZ® automatically proves that automatically produced code implements a design expressed in Simulink®. By using the ADI Ada auto-coder or the TargetLink® C auto-coder aligned to the Simulink control system subset, CLawZ produces evidence that the code correctly implements the design, or shows where the coder has made a mistake. This relieves the need to undertake unit testing thus gaining considerable time benefits.