Safety standards, such as ISO 26262, require the use of tools that ensure the completeness, correctness, and consistency of software design. In addition, it is prescribed that these tools also do not themselves introduce defects into executable code. Dezyne provides a solution to the first part of this problem, but how can a Dezyne user be certain that the behaviour of executable code derived from Dezyne models is equivalent to that of the models themselves?
ISO 26262 is concerned with the functional safety of electrical and/or electronic automotive systems. This standard requires the qualification of tools in use in the development of safety-related software. Essentially tool qualification involves making a risk assessment, where a number of factors are considered, including:
- The extent to which the tool is used in safety-critical components.
- The risk that the tool introduces errors which lead to a fault in the product.
- The chance that an introduced error passes by unnoticed.
Verum’s Dezyne toolset provides a solution to the last two of these bullets: Dezyne’s automatic formal verification eliminates entire classes of defects from the design of a software system, leading to complete, correct and consistent implementation. The various patents that Verum has on its verification technology provide a foundation for qualifying Dezyne according to the ISO standard. However, tool qualification also requires an assessment of the risk that the tool itself introduces defects into the end product. In the case of Dezyne one needs to consider whether the behaviour of the executable code that results from generating code from a Dezyne model is equivalent to that of the model itself.
Related: How Moba used Dezyne to clean up legacy software
A formal foundation for tool qualification
Verum and SolidSands have worked together to define a methodology that delivers the ultimate proof of behavioural equivalence between models and executable code. The methodology is applicable to the design and development of behaviourally complex systems. For these systems, it is very difficult to achieve an acceptable level of test coverage by any other means. While the approach is aimed at safety-critical domains it is beneficial in any domain that makes use of complex dynamic behaviour.
Further, the methodology provides a foundation for the certification of Dezyne for use in the development of safety-critical applications. Full details of this methodology are available at the link below.
Download the full case study to find out more