| 一种SCADE同步语言程序安全属性自动验证工具 |
| |
| 引用本文： | 孙毅,陈哲,冉丹,杨志斌.一种SCADE同步语言程序安全属性自动验证工具[J].小型微型计算机系统,2022(4):858-864. |
| |
| 作者姓名： | 孙毅 陈哲 冉丹 杨志斌 |
| |
| 作者单位： | 1. 南京航空航天大学计算机科学与技术学院;2. 华东师范大学上海市高可信计算重点实验室;3. 南京大学计算机软件新技术国家重点实验室 |
| |
| 基金项目： | 国家自然基金委员会-中国民航局民航联合研究基金项目(U1533130)资助；;中央高校基本科研业务费人工智能+专项项目(NZ2020019)资助；;南京大学计算机软件新技术国家重点实验室开放课题项目(KFKT2020B10)资助； |
| |
| 摘 要： | 安全关键领域的反应系统大都采用同步语言开发，然而，学术界尚不存在SCADE同步语言程序的形式化验证工具，为此，本文提出了一种自动验证SCADE同步语言程序安全属性的方法.首先使用无量词一阶逻辑公式对SCADE同步语言程序的行为进行建模，可将SCADE同步语言程序的安全属性的验证问题转化为无量词一阶逻辑公式的可满足性问题；然后采用先进的可满足性模理论求解器对其可满足性进行求解.本方法旨在实现对SCADE同步语言程序进行自动地、直接地验证，以填补SCADE同步语言程序验证领域的技术空白.此外，本文对所提方法进行了代码实现，并通过实验验证了所提方法的有效性.
|
| 关 键 词： | 反应系统 SCADE同步语言 形式化验证 一阶逻辑 可满足性模理论 |
|
