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.