Applicability of Formal Methods for Safety-Critical Systems in the Context of ISO 26262

Formal methods are a means for verification and validation with the main advantage that a system property can be verified for the overall system (including all possible system states). The drawbacks of formal methods are the additional effort for the formalisation of the requirements and for building a model of the system, and, the limitations due to computational restrictions (handling the state-space explosion). ISO 26262 “Road Vehicles - Functional Safety” is a standard for the assessment of the development process for safety-relevant components in the automotive domain. The standard addresses formal methods for the specification of safety requirements and for the product development at software level. Formal methods for the hardware development or at system level are (by now) not explicitly foreseen by the standard. In this work we will give an overview on the basic principles and the state-of-the-art of formal methods (in detail, model checking). Then we will present different approaches for the application of formal methods at system level including some preliminary evaluation results for an industrial use case. Based on these experiences we will discuss the applicabi lity of formal methods in the context of ISO 26262 (i.e., for automotive components) in view of the limitations of formal techniques for applications inthe automotive domain