A SCADE Model Verification Method Based on B-Model Transformation
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913816185405440 |
|---|---|
| author | Hou, Xili Wang, Keming Zhao, Huibing Shi, Ruiyin |
| author_facet | Hou, Xili Wang, Keming Zhao, Huibing Shi, Ruiyin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_00967 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A SCADE Model Verification Method Based on B-Model Transformation Hou, Xili Wang, Keming Zhao, Huibing Shi, Ruiyin Software Engineering Formal Languages and Automata Theory Logic in Computer Science 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. |
| title | A SCADE Model Verification Method Based on B-Model Transformation |
| topic | Software Engineering Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2505.00967 |