SCADE Model Checking Based on Program Transformation

Abstract

SCADE synchronization language is a common programming language for embedded system.It is often used to realize real-time embedded automatic control system in the research of equipment in aviation,aerospace,transportation and other safety critical fields.SCADE synchronization language is derived from the Lustre language,which adds more language structure to simplify source code.However,compared with Lustre language,the development of model checking technology of SCADE synchronous language is relatively backward.In this paper,we introduce a method and suite for model checking of SCADE programs.The core idea of the method is based on program transformation,that is,the SCADE program is finally transformed into equivalent Lustre program after lexical analysis,syntax analysis,abstract syntax tree generation,simplification,and then use JKind to complete the model checking.Moreover,we prove the correctness of the suite's model checking result by theoretical deduction and a large number of experiments.Experimental results show that the SCADE and Lustre programs with the same function produce the same model checking results,but the efficiency of SCADE is lower.

Keywords

• model checking|safe state machine|lexical analysis|syntax analysis|abstract syntax tree|jkind