Proving properties of automotive systems of systems under ISO 26262 using automated formal methods

This paper will outline the approach taken to verify properties of complex electrical/electronic systems of systems within an automotive project called PICASSOS. PICASSOS is led by Ricardo and funded by the Advanced Manufacturing Supply Chain Initiative (AMSCI). The aim of the project is to show that it is possible to automate the verification of a design at the earliest part of the development process. The project uses an electric vehicle example to show how the techniques can be used to meet the highest assurance requirements of ISO 26262 [1], i.e. ASIL D. The project has a goal of defining a process that uses formal methods and enables the supply chain to rely upon evidence produced by the process rather than relying upon a deep inspection of the product. The hypothesis is that, through the use of such high assurance techniques, the safety case is supported and costs are reduced whilst IP is protected.