This content is not included in your SAE MOBILUS subscription, or you are not logged in.
PICASSOS – Practical Applications of Automated Formal Methods to Safety Related Automotive Systems
ISSN: 0148-7191, e-ISSN: 2688-3627
Published March 28, 2017 by SAE International in United States
This content contains downloadable datasetsAnnotation ability available
PICASSOS was a UK government funded programme to improve the ability of automotive supply chains to develop complex software-intensive systems with high safety assurance and at an acceptable cost. 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 programme for enhancement and eventual commercial sale subsequently. A number of trials were undertaken comparing these two processes during simulated development of 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 a standard model-verification process at software unit level and showing how it can do so with reduced effort.
- John Botham - Ricardo UK Ltd.
- Gunwant Dhadyalla - WMG, University of Warwick
- Antony Powell - YorkMetrics Ltd.
- Peter Miller - Johnson Matthey Battery Systems
- Olivier Haas - Coventry University
- David McGeoch - Jaguar Land Rover Ltd.
- Arun Chakrapani Rao - WMG, University of Warwick
- Colin O'Halloran - University of Oxford
- Jaroslaw Kiec - Ricardo UK Ltd.
- Asif Farooq - Ricardo UK Ltd.
- Saman Poushpas - Ricardo UK Ltd.
- Nick Tudor - D-RisQ Ltd.
CitationBotham, 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, https://doi.org/10.4271/2017-01-0063.
Data Sets - Support Documents
|[Unnamed Dataset 1]|
|[Unnamed Dataset 2]|
|[Unnamed Dataset 3]|
|[Unnamed Dataset 4]|
|[Unnamed Dataset 5]|
|[Unnamed Dataset 6]|
|[Unnamed Dataset 7]|
|[Unnamed Dataset 8]|
|[Unnamed Dataset 9]|
- ISO 26262:2011. Road vehicles – Functional safety.
- Woodcock, Jim, Larsen Peter Gorm, Bicarregui Juan, and Fitzgerald John. "Formal methods: Practice and experience." ACM computing surveys (CSUR) 41, no. 4 (2009): 19.
- Clarke, Edmund M., and Wing Jeannette M.. "Formal methods: State of the art and future directions." ACM Computing Surveys (CSUR) 28, no. 4 (1996): 626-643.
- Cousot, Patrick, and Cousot Radhia. "Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints." In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 238-252. ACM, 1977.
- Huth, Michael, and Ryan Mark. Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press, 2004.
- Engel, Avner. Verification, validation and testing of engineered systems. Vol. 73. John Wiley & Sons, 2010.
- Simulink: https://uk.mathworks.com/products/simulink/
- Stateflow: https://uk.mathworks.com/products/stateflow/
- SysML: http://www.omgsysml.org/
- Modelworks: http://www.drisq.com/products-and-services/software-tools#Modelworks
- Simulink Design Verifier: https://uk.mathworks.com/products/sldesignverifier/
- EmbeddedValidator: http://www.btc-es.de/index.php?idcatside=54&lang=2
- NuSMV: http://nusmv.fbk.eu/
- Konrad, Sascha, and Cheng Betty HC. "Real-time specification patterns." In Proceedings of the 27th international conference on Software engineering, pp. 372-381. ACM, 2005.
- Sexton, D., Gilhead P., and Quadir R.. "Practical experiences of using formal requirements and their role in an overall work- flow." In System Safety Conference incorporating the Cyber Security Conference 2013, 8th IET International, pp. 1-6. IET, 2013.
- Embedded Coder: https://uk.mathworks.com/products/embedded-coder/
- Model Advisor: https://uk.mathworks.com/help/simulink/ug/consult-the-model-advisor.html
- Birch, John, Rivett Roger, Habli Ibrahim, Bradshaw Ben, Botham John, Higham Dave, Jesty Peter, Monkhouse Helen, and Palin Robert. "Safety cases and their role in ISO 26262 functional safety assessment." In International Conference on Computer Safety, Reliability, and Security, pp. 154-165. Springer Berlin Heidelberg, 2013.
- Tudor, N. J., and Botham J.. "Proving properties of automotive systems of systems under ISO 26262 using automated formal methods." In System Safety and Cyber Security (2014), 9th IET International Conference on, pp. 1-6. IET, 2014.
- Lisagor, Oleg, Sun Linling, and Kelly Tim. "The illusion of method: Challenges of model-based safety assessment." In 28th International System Safety Conference (ISSC), 2010.
- Khastgir, S., Dhadyalla, G., and Jennings, P., "Incorporating ISO 26262 Concepts in an Automated Testing Toolchain Using Simulink Design Verifier™," SAE Int. J. Passeng. Cars - Electron. Electr. Syst. 9(1):59-65, 2016, doi:10.4271/2016-01-0032
- David, Pierre, Idasiak Vincent, and Kratz Frederic. "Reliability study of complex physical systems using SysML." Reliability Engineering & System Safety 95, no. 4 (2010): 431-450.
- Mhenni, Faida, Nguyen Nga, Kadima Hubert, and Choley Jean-Yves. "Safety analysis integration in a SysML-based complex system design process." In Systems Conference (SysCon), 2013 IEEE International, pp. 70-75. IEEE, 2013.
- Lisagor, Oleg, Kelly Tim, and Niu Ru. "Model-based safety assessment: Review of the discipline and its challenges." In Reliability, Maintainability and Safety (ICRMS), 2011 9th International Conference on, pp. 625-632. IEEE, 2011.
- Joshi, Anjali, Heimdahl Mats P. E., Miller Steven P., and Whalen Mike W.. 2006. Model-Based Safety Analysis, NASA Contractor Report NASA/CR-2006-213953, Hampton, Virginia: NASA Langley Research Center
- Miller, P. “Drivewise - A vehicle with Steer-by-wire and Torque-vectoring™.” In FISITA World Automotive Congress 2008, Congress Proceedings - Electronics. FISITA, 2008.
- Miller, Peter John, Sewell Benjamin John, and Dominguez-Garcia Alejandro D.. “Method of Modelling the Effect of a Fault on the Behaviour of a System,” WIPO Patent WO2007049013, May 3, 2007.
- Andrews, Zoe, Payne Richard, Romanovsky Alexander, Didier André, and Mota Alexandre. "Model-based development of fault tolerant systems of systems." In Systems Conference (SysCon), 2013 IEEE International, pp. 356-363. IEEE, 2013.
- Blom, Hans, Lönn Henrik, Hagl Frank, Papadopoulos Yiannis, Reiser Mark-Oliver, Sjöstedt Carl-Johan, Chen De-Jiu, Tagliabò Fulvio, Torchiaro Sandra, Tucci Sara, and Kolagari Ramin T., 2013. EAST-ADL: An Architecture Description Language for Automotive Software-Intensive Systems. Embedded Computing Systems: Applications, Optimization, and Advanced Design, p.456.