基于程序转化的SCADE模型检测

SCADE同步语言是一种常用的嵌入式系统程序设计语言.在航空、航天、交通等安全关键领域的装备研发中,SCADE同步语言通常被用于实现实时嵌入式自动控制系统.SCADE语言是工业级的开发工具,它源于Lustre语言,并在其基础上增加了更多的语言结构来精简代码.目前,相比Lustre语言,SCADE程序模型检测的学术研究相对落后.为此,文中提出了一种对SCADE程序进行模型检测的方法并实现了一款SCADE模型检测工具,该方法的核心思想是基于程序转化,即把SCADE程序经过词法分析、语法分析、抽象语法树生成与化简等操作最终转化为等价的Lustre程序,然后用JKind与SMT求解器完成模型检测.此外,通过理论推导和大量实验证明了工具的模型检测的正确性.实验结果表明,功能相同的两个SCADE和Lustre测试用例模型的检测结果相同,但SCADE程序的模型检测效率相对较低.

SCADE Model Checking Based on Program Transformation