基于混成自动机的CP S行为建模与属性验证

• 作者: 周兴社 拓明福 李嘉林 李辉
• 来源期刊: 空军工程大学学报（自然科学版）
• 学科: 工学
• 关键词: 信息物理系统 模型验证 混成自动机 混合程序 模型转换
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 电子?信息?通信
• 页码范围: 40-44
• 页数: 5页
• 分类号: TP393
• 字数: 3550字
• 语种: 中文
• DOI: 10.3969/j.issn.1009-3516.2016.03.008

摘要

系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析CPS模型构建与分析验证中面临的挑战的基础上，提出了一种 CPS 行为建模与属性验证方法。该方法首先基于混成自动机对 CPS 的行为进行建模，然后将此模型转换为混合程序模型，最后在定理证明器KeYmaera中对 HP模型的属性进行形式化验证。文中论述了行为模型描述语言的结构，建立了混成自动机模型与 HP 模型之间的转换规则，分析了模型转换的一致性。应用实例表明：该方法既能简单直观地描述CPS动态行为，又能对CPS的属性进行严格的形式化验证，且有效避免了形式化验证中的状态空间爆炸问题。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周兴社	西北工业大学计算机学院	251	2217	23.0	35.0
2	李嘉林	空军工程大学理学院	23	133	6.0	11.0
3	拓明福	西北工业大学计算机学院	14	28	3.0	4.0
5	李辉	空军工程大学理学院	7	11	2.0	3.0