Rigorous verification of Automotive embedded software systems
Software based systems within automotive platforms 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 automotive domain, ISO26262 is now 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 review, analysis or test to meet ISO26262 can therefore be costly and unresponsive, even to small changes.
The use of formal methods in automotive is recognised under ISO26262 and is ‘Recommended’ for both architectures (Part4) and software (Part 6). 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 in the automotive 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 include Modelworks® and CLawZ® tackle different aspects of verification and meet tool qualification requirements under ISO26262-8 Clause 8. Our tools meet the guidance in ISO 26262-6 para 5.4.8 because the modelling and programming languages have an unambiguous definition in order to enable proof and provide appropriate level of independence.
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 distributed Systems-of Systems such as multiple platforms and Integrated Modular Avionics, as well as how architectures of more conventional systems behave.
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.