Ensuring embedded software systems are fit for purpose in the Process and Utilities Industries
Software based systems within the process industry such as plant control and electricity generation and transmission 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 this domain, IEC/ISO61508 is the key system safety document whose main aim is to achieve evidence to support the safety case. In the nuclear power industry, the standards are even more stringent with often countyr specific regulation. Gaining the required evidence from development life cycle processes that support 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/ISO61508 and nuclear standards can therefore be costly and unresponsive, even to small changes.
The use of formal methods is recognised under IEC/ISO61508 and is ‘Recommended’ for both architectures and software. In the nuclear industry, static analysis if often required to sujpport other techniques. 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 process and utilities 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 plant 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 power plant, process control or signalling, 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.