Research on Higher-Order Operator Transformation Algorithms for Syntax Transformation-Based Model Checking

Model checking technology addresses the limitations of traditional testing methods, which cannot cover all possible system states. Syntax transformation-based model checking methods convert source programs into equivalent forms and leverage existing model checking tools for verification, providing adaptability to various syntactic structures. The L2C language, widely used in safety-critical domains, lacks effective model checking support for its advanced features, particularly higher-order operators. To address this issue, this paper proposes a syntax transformation-based higher-order operator model checking method that converts L2C programs into equivalent Lustre programs. The method employs the ANTLR tool for lexical analysis, syntax analysis, abstract syntax tree generation, and simplification, enabling effective model checking of higher-order operators in the L2C language.