The verification of safety-critical systems, though supported by various tools, remains a manually intensive process, often hindered by algorithmic limitations and inadequate support for embedding safety analysis artifacts directly within design models. Techniques like model checking require formal models, which are typically created separately from the design models. This redundant modeling effort is not only time-consuming, but also introduces the risk of semantic discrepancies between the design and safety models, necessitating significant validation. To bridge this gap, this paper proposes a modeling approach to enhance the industrial applicability of automated verification techniques. We introduce a methodology for integrating key safety artifacts—specifically, Failure Modes (FMs), Failure Conditions (FCs), and analysis results like Minimal Cut Sets (MCSs)—directly into Simulink design models. This is enabled by our Design Integrated Verification Environment (DIVE) plugin, which provides specialized blocks and a workflow to connect the design environment with backend formal analysis engines. By embedding safety constructs within the design model, our approach facilitates a common ground for communication between designers and safety engineers, reduces redundant work, and lowers the barrier to adopting Model-based Safety Assessment (MBSA). The efficacy of our design-integrated verification is demonstrated through a case study of the landing gear system, illustrating the practical application of the DIVE plugin for formal safety assessment.
Gonschorek et al. (Tue,) studied this question.