Making Implicit Safety Requirements Explicit. An AUTOSAR Safety Case

Safety standards demand stringent requirements on embedded systems used in safety-critical applications such as automotive, railways, and aerospace. In the automotive domain, the AUTOSAR software architecture provides some mechanisms to fulfill the ISO26262 requirements. The verification of these mechanisms is a challenging problem and it is not always clear in which context the safety requirements are supposed to be met. In this paper, we report on a case study developed in the SafeCer project, where we combined contract-based design and model-based testing. A contract-based approach has been used to formalize the safety requirements to detect communication failures. The formal specification shows under which assumptions the AUTOSAR protection mechanism fulfills these requirements. A model-based testing approach has been used to test the software implementing such protection mechanism. The model used for testing has been model checked against the contract specification ensuring that the system-level safety requirements are met.