PICASSOS – Practical Applications of Automated Formal Methods to Safety Related Automotive Systems

J. Botham, G. Dhadyalla, A. Powell, P. Miller, Olivier Haas, D. McGeoch, A. C. Rao, C. O'Halloran, J. Kiec, A. Farooq, S. Poushpas, N. Tudor

    Research output: Contribution to journalArticlepeer-review

    4 Citations (Scopus)


    PICASSOS was a UK government funded program to improve the ability of automotive supply chains to develop demonstrably safe highly complex software-intensive systems cost effectively. This was executed by a consortium of three universities and five companies including an automotive OEM and suppliers. Three major elements of the PICASSOS project were: use of automated model based verification technology utilising formal methods; application of this technology in the context of ISO 26262; and evaluation to measure the impact of this approach to inform key management decisions on the costs, benefits and risks of applying this technology on live projects. The project spanned system level design and software development. This was achieved by using a unified model based process incorporating SysML at the system level and using Simulink and Stateflow auto-coded into C at the software level. An ISO 26262 compliant development process based on those already used by the commercial partners was used as a baseline, and a modified process using formal methods was developed. Tools that are commercially available were used wherever possible, and technology demonstrators were generated within the program. One of the program partners is enhancing these tools to make them suitable for commercial sale. A number of trials were undertaken comparing these two processes on Electric Vehicle based systems. The paper includes the results of one of the trials, showing that the formal methods based approach found errors that were missed by the standard process without significantly increasing the development time.
    Original languageEnglish
    Article number2017-01-0063
    JournalSAE Technical Paper Series
    Publication statusPublished - 28 Mar 2017

    Bibliographical note

    The full text is currently unavailable on the repository.


    • Simulation and Modeling
    • Embedded software
    • Safety critical systems
    • Electric vehicles


    Dive into the research topics of 'PICASSOS – Practical Applications of Automated Formal Methods to Safety Related Automotive Systems'. Together they form a unique fingerprint.

    Cite this