基于微分动态逻辑的CPS建模与验证
随着传感网络以及嵌入式系统等的发展，集计算、通信、控制于一体的信息CPS逐渐成为人们关注的热点。未来CPS将会应用到社会生活的各个方面，随着应用的越来越普及，CPS能否满足设计需求对系统设计实施显得至关重要。验证技术在保障和提高系统安全性、可靠性等方面起到了关键的作用，对CPS关键属性的验证也成为研究的焦点。将通用的模型转换为形式化模型进行验证是常用的验证手段，采用HybridUML对CPS进行建模，并提出一种由HybridUML向Hybrid Programs 模型进行转换的方法。Hybrid Programs是基于微分动态逻辑的定理证明方法的操作模型。最后利用转换得到的Hybrid Programs对系统实例进行验证。
信息物理融合系统 微分动态逻辑 形式化验证 模型转换
朱敏 李必信 李加凯 吉顺慧
东南大学计算机科学与工程学院 南京 211189
国内会议
长春
中文
158-163
2011-10-28（万方平台首次上网日期，不代表论文的发表时间）