SCADE Model Checking Based on Program Slicing and Multi-attribute Incremental Verification
FANG Yuyao
CHEN Zhe
Abstract：In recent years,the number of casualties and economic losses caused by software failures in the field of safety-criti-cal control systems has been increasing year by year,and the SCADE synchronous language,which is widely used in the develop-ment of safety-critical control systems,is gaining attention in program correctness verification.In order to solve the problem of low validation efficiency of existing SCADE synchronous language model checking tools,this paper proposes a model checking method based on program slicing and multi-attribute incremental detection,which simplifies the verified program by removing attribute-in-dependent data streams and equations with the program slicing algorithm,and speeds up the verification by reusing intermediate ver-ification results with the multi-attribute incremental verification algorithm.Finally,a model checking tool for SCADE synchronous language programs is implemented.The tool implements an optimization algorithm to improve the efficiency of SCADE synchronous language model checking based on a parallel verification architecture.The results show that the proposed optimization method can ef-fectively and automatically verify SCADE synchronous language programs and improve the verification efficiency of model checking by about 15%.
Keywords：synchronous languagesafety-critical control systemmodel checkingprogram verification
Publication Date：2025-10-20
Online Publishing Date：2026-01-16(First online date of this platform, not the publication date of the document)
Pages：6( 2728-2732,2823 )