基于混成自动机的CP S行为建模与属性验证
拓明福1
周兴社2
李嘉林3
李辉3
1.西北工业大学计算机学院，西安，710129; 空军工程大学理学院，西安，7100512.西北工业大学计算机学院，西安，7101293.空军工程大学理学院，西安，710051
摘要：系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析CPS模型构建与分析验证中面临的挑战的基础上，提出了一种 CPS 行为建模与属性验证方法。该方法首先基于混成自动机对 CPS 的行为进行建模，然后将此模型转换为混合程序模型，最后在定理证明器KeYmaera中对 HP模型的属性进行形式化验证。文中论述了行为模型描述语言的结构，建立了混成自动机模型与 HP 模型之间的转换规则，分析了模型转换的一致性。应用实例表明：该方法既能简单直观地描述CPS动态行为，又能对CPS的属性进行严格的形式化验证，且有效避免了形式化验证中的状态空间爆炸问题。
关键词：信息物理系统模型验证混成自动机混合程序模型转换
分类号：TP393(计算技术、计算机技术)
资助基金：国家自然科学基金(61472443)
论文发表日期：2016-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：5( 40-44 )
英文信息