A SCADE Model Verification Method Based on B-Model Transformation

TL;DR

This paper introduces a formal verification framework that transforms SCADE models into B models, enabling more effective verification of abstract specifications in safety-critical systems, with improved defect detection and efficiency.

Contribution

It establishes a semantic equivalence transformation from SCADE to B models, addressing key technical challenges and enhancing verification capabilities for complex safety-critical system specifications.

Findings

Higher defect detection rate in B models

Improved verification efficiency in ProB environment

Effective verification of complex abstract specifications

Abstract

Due to the limitations of SCADE models in expressing and verifying abstract specifications in safety-critical systems, this study proposes a formal verification framework based on the B-Method. By establishing a semantic equivalence transformation mechanism from SCADE models to B models, a hierarchical mapping rule set is constructed, covering type systems, control flow structures, and state machines. This effectively addresses key technical challenges such as loop-equivalent transformation proof for high-order operators and modeling of temporal logic storage structures. The proposed method innovatively leverages the abstraction capabilities of B-Method in set theory and first-order logic, overcoming the constraints of native verification tools of SCADE in complex specification descriptions. It successfully verifies abstract specifications that are difficult to model directly in SCADE. Experimental results show that the transformed B models achieve a higher defect detection rate and improved verification efficiency in the ProB verification environment compared to the native verifier of SCADE, significantly enhancing the formal verification capability of safety-critical systems. This study provides a cross-model verification paradigm for embedded control systems in avionics, rail transportation, and other domains, demonstrating substantial engineering application value.