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.
Applicability of Formal Methods for Safety-Critical Systems in the Context of ISO 26262 / Kandl, Susanne; Elshuber, Martin; Gulan, Stefan; Nguyen, Thang; Rieger, Stefan; Schrammel, Peter; Sisto, Riccardo. - STAMPA. - 23:(2015), pp. 95-115. (Intervento presentato al convegno Safety-critical Systems Symposium tenutosi a Bristol (UK) nel 3rd-5th February 2015).
Applicability of Formal Methods for Safety-Critical Systems in the Context of ISO 26262
SISTO, Riccardo
2015
Abstract
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.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/2616709
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo