A Fault Injection and Formal Verification Framework Based on UML Sequence Diagrams

Previous studies suggest that the combination of model-based fault injection and model checking can effectively detect the dependability bottlenecks and verify the fault-tolerance capability of systems at very early phases of their lifecycles. However, a challenge of applying such techniques in the industry is that semi-formal modeling languages like UML cannot easily support automated analysis and formal verification. To address this challenge, we propose a fault injection and verification framework based on UML sequence diagrams. The idea is to create formal models from sequence diagrams as well as predefined fault models, and then run a model checker to check if specific properties are violated. With an exhaustive exploration of a system's states and fault space by the model checker, the approach ensures complete, automated reasoning on failure modes and effects. The framework also allows the designs of additional recovery actions to tolerate faults and then the verification of the updated models. The framework separates manual and automated activities, providing a guide to the practices of developers and the development of the support tool. We conduct a study on an industrial case and demonstrate that by the proposed approach, critical design flaws are revealed.