Beschreibung:
<jats:title>Abstract</jats:title><jats:p>There is an increasing trend towards model‐based development (MBD) of safety‐critical systems. In an MBD approach, various development activities such as simulation, testing, code generation, and verification are based on a single formal model of the system. In this paper we show that the MBD approach can also be applied towards automating the safety analysis process. Using precise formal models of the system as the basis of the analysis helps avoiding design errors at early stages in the development lifecycle. The analysis is automated by means of model‐checking tools, which results in a more thorough analysis and reduced manual effort compared to more traditional methods. We illustrate model‐based analysis using the fault‐tolerant startup protocol for a time‐triggered middleware architecture (TTA). For a functional model of this protocol, it is verified that the specified safety requirements are satisfied in the presence of all faults within the given fault hypothesis. We demonstrate that exact, complete, and consistent safety analyses can—and in fact should—be carried out for relevant industrial designs in very early phases of the development life cycle and in an automated fashion.</jats:p>