计算机科学与探索2026，Vol.20Issue(7)：1954-1962,9.DOI:10.3778/j.issn.1673-9418.2509006
面向SCADE高阶语言结构的程序转换和模型检验技术
Program Transformation and Model Checking Techniques for Higher-Order Lan-guage Constructs in SCADE
摘要
Abstract
Synchronous dataflow languages are widely used in safety-critical systems,such as the Lustre and SCADE(safety critical application development environment).Compared with Lustre,SCADE introduces various higher-order programming constructs that enhance usability and expressiveness.The safety verification of safety-critical systems relies on model checking to perform formalized system proofs.However,existing verification tools for SCADE have limita-tions:do not fully support all higher-order constructs,verification capabilities are restricted to XML structures.As a result,their ability to verify large and complex programs remains limited.This paper focuses on model checking for SCADE pro-grams containing higher-order language constructs(including 12 types of higher-order iterators such as map and fold,and parameterized nodes).A semantic equivalence-based translation algorithm is proposed to transform higher-order language constructs into Lustre programs,after which existing tools are utilized to perform model checking on the translated programs.Furthermore,the concept of clocked dataflow equivalence is introduced to evaluate the semantic equivalence between the original and translated programs.Experiments are conducted on a SCADE test containing higher-order language constructs,and the results demonstrate the effectiveness of the proposed model checking tool based on the translation algorithm.The approach successfully enables model checking for programs involving higher-order language structures.In summary,the proposed method enhances the language compatibility and verification capability of SCADE model checking.关键词
SCADE/高阶迭代器/参数化节点/程序转换/模型检验Key words
SCADE/higher-order iterator/parameterized node/program transformation/model checking分类
信息技术与安全科学引用本文复制引用
王慧杰,陈哲,韦依洋..面向SCADE高阶语言结构的程序转换和模型检验技术[J].计算机科学与探索,2026,20(7):1954-1962,9.基金项目
国家自然科学基金(62172217) （62172217）
国家自然科学基金委员会-中国民航局民航联合研究基金(U1533130). This work was supported by the National Natural Science Foundation of China(62172217),and the National Natural Science Founda-tion of China and Civil Aviation Administration of China(U1533130). （U1533130）
