Formalized Failure Propagation Analysis for Safety-Critical Systems: From SysML/SafeDeML to Automated Safety Verification

Problem Statement

While embedding safety information directly into system models closes the gap between design and safety analysis documents, it does not inherently provide a mechanism for computational analysis. Analyzing how a fault in one component propagates through interfaces to cause failures in other parts of the system is often a manual, error-prone, and non-scalable task. To achieve a higher degree of confidence and automation, the semi-formal semantics of the SysML/SafeDeML model must be mapped to a formal model with well-defined compositional semantics, such as Component Fault Trees (CFTs) or another suitable formalism. This transformation would enable the use of powerful formal analysis techniques to automatically identify critical failure chains and verify that the system design, including its safety mechanisms, is robust against hardware faults.

Research Questions

1. How can a formal semantics be defined for the core elements of the SafeDeML profile (Fault, Failure, Diagnosis, Port) to enable a sound and automated transformation into a compositional safety analysis formalism like Component Fault Trees?

2. How can an automated model transformation workflow be implemented to translate a SysML model, annotated with SafeDeML, into a system-level formal model suitable for failure propagation analysis?

3. How can the results from the formal analysis (e.g., minimal cut sets for a top-level safety goal violation) be automatically computed and traced back to the source SysML model to provide actionable feedback to system designers?

Methodology

1. Literature Review and Formalism Selection: Conduct a focused review of formalisms for model-based safety analysis, including Component Fault Trees (CFT), HiP-HOPS, and state-based formalisms (e.g., stochastic automata). The primary candidate for selection will be CFTs due to their inherent compositionality, which aligns well with the block-based, hierarchical structure of SysML.

2. Mapping and Transformation Definition: Define a formal mapping from the SafeDeML/SysML metamodel to the selected formal metamodel (e.g., CFT). This will specify how SysML blocks containing SafeDeML::Fault and SafeDeML::Failure elements are translated into basic events, logic gates, and input/output failure ports of a component model. The propagation semantics defined via SafeDeML::Port connections will guide the composition of these component models.

3. Prototypical Implementation: Implement the defined model transformation as a software tool, for example, as a plugin for a CASE tool like Enterprise Architect or Cameo Systems Modeler. This tool will parse the annotated SysML model, generate the corresponding formal model (e.g., in the xSAP or an equivalent format), and interface with an existing backend analysis engine to perform the safety analysis.

4.  

   Case Study and Evaluation: Apply the implemented toolchain to a representative safety-critical system, such as the brake-light controller example presented in the source paper. The evaluation will focus on the correctness of the generated analysis, the scalability of the approach for larger models, and the utility of tracing analysis results back to the design artifacts.

 

Student Opportunities

• Model-Based Engineering (MBE): Gain deep, practical experience in SysML, model transformations (QVT/ATL), and the development of domain-specific languages (DSLs) like SafeDeML.

• Functional Safety and Formal Methods: Apply foundational concepts from functional safety (ISO 26262) and formal methods (Fault Tree Analysis, Model Checking) to solve a practical engineering problem.

• Software and Systems Engineering: Develop a robust software tool within a research context, contributing to a tangible artifact that bridges the gap between system design and formal verification.

• Agile Research: Collaborate within a research team using agile methodologies for project management and iterative development.

Significance

This project directly addresses the critical challenge of ensuring the correctness and completeness of safety analyses in modern MBSE workflows. By creating a formal bridge between the system design and safety analysis domains, this work will enable designers to receive rapid, automated, and rigorous feedback on the safety implications of their design decisions. The resulting methodology and toolchain will contribute to building more reliable and trustworthy safety-critical systems, reducing manual effort and the risk of human error in safety assessment.

Significant References for Foundational Knowledge

• On SafeDeML and SysML-based Safety Design:

  • Gonschorek, T., Bergt, P., Filax, M., & Ortmeier, F. (2019). SafeDeML: On Integrating the Safety Design into the System Model. In Computer Safety, Reliability, and Security (pp. 271-285). Springer. 

• On General Functional Safety and Model-Based Safety Analysis (MBSA):

  • ISO 26262:2018. Road vehicles — Functional safety. International Organization for Standardization.

  • Papadopoulos, Y., & McDermid, J. A. (1999). Hierarchically Performed Hazard Origin and Propagation Studies. In Computer Safety, Reliability, and Security (pp. 139-152). Springer. (Introduces the core concepts of the HiP-HOPS methodology).

  • Weilkiens, T. (2007). Systems Engineering with SysML/UML: Modeling, Analysis, Design. Morgan Kaufmann. (Provides foundational knowledge on SysML).