Practical Applications of Formal Methods in Automotive Functional Safety

The increasing scale and complexity of electrical/electronic systems in modern automotive systems imposes a growing challenge in maintaining their reliability and safety within the constraints of time-to-market and acceptable costs.

PICASSOS (Proving Integrity of Automotive Systems of Systems) was a UK government funded industrial research program set up to develop new approaches to the design of complex networks of electrical/electronic components on vehicles. The program was executed by a consortium that included three universities and five commercial organisations; these included an OEM and suppliers from the automotive industry, a tool vendor and a specialist in metrics.

The objective of the program was to improve the industry’s ability to develop demonstrably safe systems in a timely and cost effective way. It aimed to do this by demonstrating how, pragmatically, to bring the rigour of formal methods to improve existing practices within automotive supply chains; and thereby to improve the ability of the industry to deliver complex systems with very high levels of safety assurance. A secondary aim of the program was to quantify the costs and benefits of these approaches to support their uptake.

The approach taken within PICASSOS was to focus on the practical applicability within commercial production contexts of technologies and techniques based on formal methods. Tools that are commercially available and supported were used wherever possible. Technology demonstrators were also generated within the program; one of the program partners is enhancing these demonstrators to make them suitable for commercial sale beyond the program. A guiding principle was to make the techniques usable by typical systems, safety and software engineers with no background in formal methods.

Additionally, new techniques based on formal methods were compared back-to-back with traditional approaches. Data were gathered to provide objective evidence of their relative effectiveness and cost. The purpose of this was to generate metrics to permit individual organisations to make reasoned decisions over the adoption of the new techniques onto live projects; assessing the project risk of doing so in light of their known costs and benefits.

SAE International World Congress

The PICASSOS project team are presenting a technical paper at the SAE World Conference in Detroit, 4th-6th April 2017.

Botham, J., Dhadyalla, G., Powell, A., Miller, P. et al., "PICASSOS - Practical Applications of Automated Formal Methods to Safety Related Automotive Systems," SAE Technical Paper 2017-01-0063, 2017, doi:10.4271/2017-01-0063.

The PICASSOS Formal Methods Seminar Proceedings

The PICASSOS Formal Methods Seminar was held on the 28th February 2017 at the British Motor Museum.  The proceedings of the seminar outline the key findings of the project and are now available for free download.


The further dissemination of this document is encouraged, however the information contained within is not to be disseminated in any other form without appropriate attribution.  Any party making use of the contents of this document must rely on their own judgement when doing so.  The PICASSOS consortium members accept no liability for consequences arising from this document’s being relied upon by any third party.

PICASSOS partners

The PICASSOS project (Proving Integrity of Complex Automotive Systems of Systems) is part-funded by the UK's Advanced Manufacturing Supply Chain Initiative (AMSCI) and is a collaboration led by Ricardo, with partners Jaguar Land Rover, Johnson Matthey Battery Systems, YorkMetrics, D-RisQ and the universities of Oxford, Coventry and Warwick.

Further documents

Further project material will be posted in the coming weeks.

To find out more, or to be added to our mailing list, please email: [email protected]