%0 Journal Article
%T 基于微分动态逻辑的CPS建模与属性验证
%A 朱敏
%A 李必信
%A 陈乔乔
%A 吉顺慧
%A 李加凯
%J 电子学报
%P 1126-1132
%D 2012
%R 10.3969/j.issn.0372-2112.2012.06.010
%X 随着信息物理融合系统(Cyber-PhysicalSystems,CPS)应用的越来越普及,CPS的设计和实现能否满足实际需求显得至关重要.本文提出了一种CPS建模与属性验证框架.在框架中,首先使用HybridUML对CPS进行建模,然后将该通用模型转换为形式化模型,进而进行形式化验证.本文采用的形式化验证方法为dL(DifferentialDynamicLogic),其操作模型为hybridprogram.将HybridUML模型转换为hybridprogram时,基于语义一致性的原则定义转换规则.转换完成后,结合得到的hybridprogram对验证的CPS属性进行规约,最后使用定理证明器KeYmaera对属性进行自动化验证.
%K 信息物理融合系统
%K 微分动态逻辑
%K HybridUML
%K 模型转换
%K 验证
%U http://www.ejournal.org.cn/CN/abstract/abstract6567.shtml