Can formal methods make automotive business sense? A classification of formal methods

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.