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
ISSN: 0148-7191, e-ISSN: 2688-3627
Published April 14, 2008 by SAE International in United States
Annotation ability available
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  .
The automotive industry is responding to the increasing impact of automotive software with the development of standards such as AUTOSAR , and EU funded projects such as ATESST  and EASIS . 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 , 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.
|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|
CitationMcElligott, 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.
- Airbus, Airbus Financial Statements and Corporate Governance 2005 -http://www.eads.net/xml/content/OF00000000400004/2/73/41323732.pdf. 2006.
- VolkswagenAG, VolkswagenAG 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.
- KienckeU., NielsenL., and KGS.-V.B.a.H.G.C., Automotive Control Systems: For Engine, Driveline And Vehicle. 2000: Springer-Verlag Berlin and Heidelberg GmbH & Co. KG. 427
- BechmannO., et al., Particulate emissions and their measurement in practice:Today and in the future. http://www.oica.net/htdocs/Main.htm, 2002.
- SchauffeleJ. and ZurawkaT. Automotive Software Engineering: Principles, Processes, Methods, and Tools 2005: SAE International 408
- SMCS (2006) Multimedia Networking - MOST Summary Volume,
- BroyM., 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.
- PretschnerA. et al. Software Engineering for Automotive Systems: A Roadmap in 2007 Future of Software Engineering 2007: IEEE Computer Society.
- KitchenhamB. et al., Guidelines for performing Systematic Literature Reviews in Software Engineering, in EBSE Technical Report. 2007, Software Engineering Group School of Computer Science and Mathematics Keele University.
- BowenJ.P. and HincheyM.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.
- BowenJ.P. and HincheyM.G. Ten commandments of formal methods… ten years later, in Computer 2006. p. 40-48
- OliveiraJ.N., A Survey of Formal Methods Courses in European Higher Education. LNCS, 2004. 3294: p. 235-248.
- SWEBOK, Guide to the Software Engineering Body of Knowledge (SWEBOK), ed. AbranA., et al. 2004: IEEE Computer Society.
- WingJ.M., A Specifier's Introduction to Formal Methods. IEEE Computer, 1990. 23: p. 8-24.
- SommervilleI., Software Engineering. 1992: Addison-Wesley.
- PressmanR.S., Software Engineering: A Practitioner's Approach. 2004: McGraw-Hill.
- SommervilleI., Software Engineering. 2001: Addison-Wesley.
- ClarkeE.M. and WingJ.M. Formal methods: state of the art and future directions. Vol. 28. 1996: ACM Press. 626-643.
- BowenJ.P. and HincheyM.G. Ten Commandments of Formal Methods. IEEE Computer, 1995. 28(4): p. 56-63.
- BowenJ. (2005) Formal Methods: a Virtual Library - http://vl.fmnet.info/. Volume,
- RushbyJ., 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.
- CaspiP. 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.
- AbrialJ.-R., The B-Book: Assigning Programs to Meanings 1996: Cambridge University Press. 850
- TurnerK.J., Using Formal Description Techniques: An Introduction to Estelle, Lotos, and SDL. 1993: John Wiley \& Sons, Inc. 460.
- van EijkP.H.J., VissersC.A., and DiazM. 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/.
- SchumannJ.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.
- DenneyR., A Comparison of the Model-Based & Algebraic Styles of Specification as a Basis for Test Specification. ACM Sigsoft, 1996. 21(5): p. 60-64.
- BurchJ.R., et al., Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems 1994.
- BehmP., et al. Meteor:A Successful Application of B in a Large Project. in FM'99. 1999: LNCS Springer-Verlag.
- MilnerR., A Calculus of Communicating Systems. 1980: Springer Verlag.
- HoareC.A.R., Communicating sequential processes. 1978.
- LarsenK.G., PetterssonP., and WangY. 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.
- YovineS., Kronos: a verification tool for real-time systems. Journal on Software Tools for Technology Transfer, 1997. 1(1-2): p. 123-133.
- BordbarB. and OkanoK. Verification of Timeliness QoS Properties in Multimedia Systems. in 5th International Conference on Formal Engineering Methods (ICFEM 2003) LNCS 2885. 2003.
- LindahlM., PetterssonP., and YiW. Formal Design and Analysis of a Gear Controller. Springer International Journal of Software Tools for Technology Transfer (STTT), 2001. 3: p. 353-368.
- LeenG. and HeffernanD. 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.
- AltisenK. et al. A framework for scheduler synthesis in 20th IEEE Real-Time Systems Symposium, 1999 1999. Phoenix, AZ, USA 1-3rd Dec., 1999
- AlurR. et al., The algorithmic analysis of hybrid systems.. Theoretical Computer Science, 1995. 138 p. 3-34.
- HenzingerT.A., et al. What's decidable about hybrid automata? in 27th Annual Symposium on Theory of Computing. 1995: ACM Press.
- LafferriereG., PappasG.J., and YovineS., A new class of decidable hybrid systems in Hybrid Systems: Computation and Control, VaandragerF.W. and SchuppenJ.v., Editors. 1999, Springer. p. 103-116.
- HenzingerT.A., Pei-HsinH., and Wong-ToiH. HyTech: A Model Checker for Hybrid Systems. International Journal on Software Tools for Technology Transfer (STTT), 1997. 1, Numbers 1-2: p. 110-122.
- KurzhanskiA. and VaraiyaP., Ellipsoidal techniques for reachability analysis, in Hybrid Systems: Computation and Control, LynchN. and KroghB., Editors. 2000, Springer. p. 203-213.
- ChutinanA. and KroghB.H., Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations, in Hybrid Systems: Computation and Control, VaandragerF.W. and SchuppenJ.v., Editors. 1999, Springer Verlag. p. 76-90.
- MalerO. and PnueliA., Hybrid Systems: Computation and Control 6th International Workshop, HSCC 2003. Vol. LNCS 2623. 2003: Springer.
- BadeauF. and AmelotA. Using B as a High Level Programming Language in an Industrial Project: Roissy VAL. in ZB 2005: LNCS
- BidoitM. and MossesP.D. CASL Use Manual Introduction to Using the Common Algebraic Specification Language. Lecture Notes in Computer Science, ed. Gerhard GoosK.U., GermanyC.U. HartmanisJuris, NY, USA, and U.U. Jan van Leeuwen, The Netherlands. Vol. 2900. 2004, Berlin Heidelberg NewYork: Springer-Verlag
- studies, L.c., http://www.inrialpes.fr/vasy/pub/cadp/case-studies/
- LeavensG.T., BakerA.L., and RubyC., Preliminary Design of JML: A Behavioral Interface Specification Language for Java.ACM SIGSOFT Software Engineering Notes, 2006. 31(3): p. 1-38.
- RustanK. et al., ESC/Java user's manual. Technical note. 2000, Compaq Systems Research Center, .
- ESC/JAVA2, http://secure.ucd.ie/products/opensource/ESCJava2/.