This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Can Formal Methods Make Automotive Business Sense? A Classification of Formal Methods by Usefulness
Technical Paper
2008-01-0119
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
Legislative bodies are directing that automotive products comply with stringent safety levels. The liability for the safety of passengers in an automobile has traditionally been quite complex. Other transport sectors are externally regulated, and liability lies with the manufacturer or the transport service provider. The automotive industry is self-regulated and the individual driver carries a significant liability.
Software and electronics increasingly provide greater control of automotive safety, possibly reducing driver liability, and increasing the need for more formal software development methods. The automotive business model, however, also presents challenges to the effective use of formal methods. An automotive design change costing €600 per vehicle could consume 100% of gross margin. In aviation, this cost represents 0.01% of gross margin [1] [2].
The automotive industry is responding to the increasing impact of automotive software with the development of standards such as AUTOSAR [3], and EU funded projects such as ATESST [4] and EASIS [5]. They propose architectures which might deliver the benefits of best software engineering practice to the industry. In terms of safety, they recommend existing accepted standards such as IEC61508 [6], which stipulates various formal methods for the development of safety-critical software. However, IEC61508 does not compare specific formal methods in terms of their suitability to industry.
This paper discusses the suitability for industry of formal methods of specification and verification. It provides a classification which looks at categories such as commercialization; capacity to solve industry-scale problems; cost effectiveness, etc. The paper looks at the relevance of the classification in terms of the challenges and constraints of the automotive domain and discusses how it might facilitate the engineer to make design decisions which improve safety in a cost effective manner.
Recommended Content
| Journal Article | Software Product Lines in Automotive Systems Engineering |
| Technical Paper | Open Source Platforms Challenge Traditional Proprietary IVI Systems |
| Technical Paper | Hardware/Software Co-Design of an Automotive Embedded Firewall |
Authors
Topic
Citation
McElligott, P., Mjeda, A., and Thiel, S., "Can Formal Methods Make Automotive Business Sense? A Classification of Formal Methods by Usefulness," SAE Technical Paper 2008-01-0119, 2008, https://doi.org/10.4271/2008-01-0119.Also In
References
- Airbus, Airbus Financial Statements and Corporate Governance 2005 http://www.eads.net/xml/content/OF00000000400004/2/73/41323732.pdf 2006
- Volkswagen AG Volkswagen AG Annual Report 2005 http://www.volkswagen.co.uk/company/annual_reports 2005
- AUTOSAR. Automotive Open System Architecture 2007 [cited; Available from: http://www.autosar.org/find02.php
- ATESST. Advancing Traffic Efficiency and Safety Through Software Technology 2007 [cited; Available from: http://www.atesst.org/scripts/home/publigen/content/templates/show.asp?P=112&L=EN&ITEMID=2
- EASIS. Electronic Architecture and System Engineering for Integrated Safety Systems 2007 [cited; Available from: http://www.easis-online.org/wEnglish/overview/index.shtml?navid=1
- IEC61508, Functional Safety of Electrical/Electronic/Programmable Electronic Safety-related Systems (IEC 61508) 1998 International Electrotechnical Commission, 3 rue de Varembé Geneva, Switzerland
- Kiencke U. Nielsen L. KG S.-V.B.a.H.G.C. Automotive Control Systems: For Engine, Driveline And Vehicle 2000 Springer-Verlag Berlin and Heidelberg GmbH & Co. KG. 427
- Bechmann O. et al. Particulate emissions and their measurement in practice:Today and in the future http://www.oica.net/htdocs/Main.htm 2002
- Schauffele J. Zurawka T. Automotive Software Engineering: Principles, Processes, Methods, and Tools 2005 SAE International 408
- SMCS 2006 Multimedia Networking - MOST Summary Volume
- Broy M. Challenges in automotive software engineering in Proceeding of the 28th international conference on Software engineering 2006 ACM Press Shanghai, China
- General_Motors_Corporation, Anuual Report 2005 Advertising and Research and Development page 107 2005
- General_Motors_Corporation, SEC Commission file number 1-143 GENERAL MOTORS CORPORATION 2006 U.S. Securities Exchange Commission Washington, DC
- Toyota, Toyota Motor Corporation Annual Report 2006 http://www.toyota.co.jp/en/ir/library/ 2006
- Boeing_Corporation, Vision 2016: Annual report 2005 http://www.boeing.com/companyoffices/financial/finreports/annual/05annualreport/index.html 2005
- Airbus, Leading Edge: Airbus Annual Report 2005 http://www.reports.eads.net/2005/ar_2005/en/s/downloads/files/annual_review_eads_ar05.pdf 2006
- Pretschner A. et al Software Engineering for Automotive Systems: A Roadmap in 2007 Future of Software Engineering 2007 IEEE Computer Society
- Kitchenham B. et al Guidelines for performing Systematic Literature Reviews in Software Engineering EBSE Technical Report 2007 Software Engineering Group School of Computer Science and Mathematics Keele University
- Bowen J.P. Hinchey M.G. Ten commandments revisited: a ten-year perspective on the industrial application of formal methods in Proceedings of the 10th international workshop on Formal methods for industrial critical systems FMICS ‘05 2005 Lisbon
- Bowen J.P. Hinchey M.G. Ten commandments of formal methods… ten years later, in Computer 2006 40 48
- Oliveira J.N. A Survey of Formal Methods Courses in European Higher Education LNCS 2004 3294 235 248
- SWEBOK, Guide to the Software Engineering Body of Knowledge (SWEBOK) Abran A. et al 2004 IEEE Computer Society
- Wing J.M. A Specifier's Introduction to Formal Methods IEEE Computer 1990 23 8 24
- Sommerville I. Software Engineering 1992 Addison-Wesley
- Pressman R.S. Software Engineering: A Practitioner's Approach 2004 McGraw-Hill
- Sommerville I. Software Engineering 2001 Addison-Wesley
- Clarke E.M. Wing J.M. Formal methods: state of the art and future directions 28 1996 ACM Press 626 643
- Bowen J.P. Hinchey M.G. Ten Commandments of Formal Methods IEEE Computer 1995 28 4 56 63
- Bowen J. 2005 Formal Methods: a Virtual Library http://vl.fmnet.info/ . Volume
- Rushby J. Harnessing Disruptive Innovation in Formal Verification in Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods 2006 IEEE Computer Society
- B-Atelier http://www.atelierb.societe.com/index_uk.html . [cited; Available from: http://www.atelierb.societe.com/index_uk.html
- B-Toolkit http://www.b-core.com/btoolkit.html . [cited; Available from: http://www.b-core.com/btoolkit.html
- PRAXIS http://www.praxis-his.com/
- ESTEREL-TECHNOLOGIES Scade http://www.esterel-technologies.com/ . [cited.
- Caspi P. et al Lustre: a declarative language for programming synchronous systems . in 14th ACM Conf. on Principles of Programming Languages 1987 Munich
- ESCHER-TECHNOLOGIES Perfect Developer , http://www.eschertech.com/papers/safe_oo_software.pdf
- ESC/Java http://secure.ucd.ie/products/opensource/ESCJava2/
- AUTOFOCUS http://autofocus.informatik.tu-muenchen.de/index-e.html
- Abrial J.-R. The B-Book: Assigning Programs to Meanings 1996 Cambridge University Press 850
- Turner K.J. Using Formal Description Techniques: An Introduction to Estelle, Lotos, and SDL 1993 John Wiley \& Sons, Inc. 460
- van Eijk P.H.J. Vissers C.A. Diaz M. The Formal Description Technique LOTOS 1989 Elsevier
- SRI, PVS http://pvs.csl.sri.com/
- ISABELLE http://www.cl.cam.ac.uk/research/hvg/Isabelle/
- KIV http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/kiv/
- Schumann J.M. Automated theorem proving in software engineering 2001 Springer-Verlag New York, Inc. 228
- PROVER-TECHNOLOGY Prover Plug-In http://www.prover.com/products/ppi/ . [cited.
- Denney R. A Comparison of the Model-Based & Algebraic Styles of Specification as a Basis for Test Specification ACM Sigsoft 1996 21 5 60 64
- Burch J.R. et al. Symbolic model checking for sequential circuit verification IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems 1994
- Behm P. et al Meteor:A Successful Application of B in a Large Project. in FM'99 1999 LNCS Springer-Verlag
- Milner R. A Calculus of Communicating Systems 1980 Springer Verlag
- Hoare C.A.R. Communicating sequential processes 1978
- Larsen K.G. Pettersson P. Wang Y. Compositional and symbolic model-checking of real-time systems in Proceedings of the 16th IEEE Real-Time Systems Symposium (RTSS ‘95) 1995 IEEE Computer Society
- Yovine S. Kronos: a verification tool for real-time systems Journal on Software Tools for Technology Transfer 1997 1 1-2 123 133
- Bordbar B. Okano K. Verification of Timeliness QoS Properties in Multimedia Systems in 5th International Conference on Formal Engineering Methods (ICFEM 2003) LNCS 2885 2003
- Lindahl M. Pettersson P. Yi W. Formal Design and Analysis of a Gear Controller Springer International Journal of Software Tools for Technology Transfer (STTT) 2001 3 353 368
- Leen G. Heffernan D. Modeling and Verification of a Time-triggered Networking Protocol in International Conference on Networking/International Conference on Systems/International Conference on Mobile Communications and Learning Technologies ICN/ICONS/MCL 2006 23-29 April 2006 Mauritius
- Altisen K. et al A framework for scheduler synthesis in 20th IEEE Real-Time Systems Symposium, 1999 1999 Phoenix, AZ, USA 1-3rd Dec 1999
- Alur R. et al The algorithmic analysis of hybrid systems Theoretical Computer Science 1995 138 3 34
- Henzinger T.A. et al What's decidable about hybrid automata? 27th Annual Symposium on Theory of Computing 1995 ACM Press
- Lafferriere G. Pappas G.J. Yovine S. A new class of decidable hybrid systems in Hybrid Systems: Computation and Control Vaandrager F.W. Schuppen J.v. 1999 Springer 103 116
- Henzinger T.A. Pei-Hsin H. Wong-Toi H. HyTech: A Model Checker for Hybrid Systems International Journal on Software Tools for Technology Transfer (STTT) 1997 1 Numbers 1-2 110 122
- Kurzhanski A. Varaiya P. Ellipsoidal techniques for reachability analysis in Hybrid Systems: Computation and Control Lynch N. Krogh B. 2000 Springer 203 213
- Chutinan A. Krogh B.H. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations in Hybrid Systems: Computation and Control Vaandrager F.W. Schuppen J.v. 1999 Springer Verlag 76 90
- Maler O. Pnueli A. Hybrid Systems: Computation and Control 6th International Workshop, HSCC 2003 2623 2003 Springer
- Badeau F. Amelot A. Using B as a High Level Programming Language in an Industrial Project: Roissy VAL. in ZB 2005 LNCS
- Bidoit M. Mosses P.D. CASL Use Manual Introduction to Using the Common Algebraic Specification Language Lecture Notes in Computer Science Gerhard Goos K.U. Germany C.U. Hartmanis Juris NY, USA, and U.U. Jan van Leeuwen, The Netherlands 2900 2004 Berlin Heidelberg NewYork Springer-Verlag
- studies, L.c. http://www.inrialpes.fr/vasy/pub/cadp/case-studies/
- Leavens G.T. Baker A.L. Ruby C. Preliminary Design of JML: A Behavioral Interface Specification Language for Java ACM SIGSOFT Software Engineering Notes 2006 31 3 1-38
- Rustan K. et al ESC/Java user's manual Technical note 2000 Compaq Systems Research Center
- ESC/JAVA2 http://secure.ucd.ie/products/opensource/ESCJava2/