面向SCADE高阶语言结构的程序转换和模型检验技术OA

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.