基于微分动态逻辑的CPS建模与属性验证

朱敏; 李必信; 陈乔乔; 吉顺慧; 李加凯

doi:10.3969/j.issn.0372-2112.2012.06.010

您当前的位置：

首页 >

文章列表页 >

基于微分动态逻辑的CPS建模与属性验证

学术论文 | 更新时间：2025-07-16

- 基于微分动态逻辑的CPS建模与属性验证
- Transforming HybridUML to Hybrid Program for CPS Property Verification
- 电子学报 2012年40卷第6期页码：1126-1132
- 作者机构：
  
  东南大学计算机科学与工程学院,江苏,南京,211189
- 作者简介：
- 基金信息：
  
  国家自然科学基金 (No.60973149);博士点基金 (No.20100092110022);中科院计算机科学国家重点实验室开放基金基金 (No.SYSKF1110)
- DOI：10.3969/j.issn.0372-2112.2012.06.010
  中图分类号： TP301
- 纸质出版：2012
- 稿件说明：
移动端阅览
朱敏, 李必信, 陈乔乔, 等. 基于微分动态逻辑的CPS建模与属性验证[J]. 电子学报, 2012,40(6):1126-1132.

ZHU Min, LI Bi-xin, CHEN Qiao-qiao, et al. Transforming HybridUML to Hybrid Program for CPS Property Verification[J]. Acta Electronica Sinica, 2012, 40(6): 1126-1132.
朱敏, 李必信, 陈乔乔, 等. 基于微分动态逻辑的CPS建模与属性验证[J]. 电子学报, 2012,40(6):1126-1132. DOI： 10.3969/j.issn.0372-2112.2012.06.010.

ZHU Min, LI Bi-xin, CHEN Qiao-qiao, et al. Transforming HybridUML to Hybrid Program for CPS Property Verification[J]. Acta Electronica Sinica, 2012, 40(6): 1126-1132. DOI： 10.3969/j.issn.0372-2112.2012.06.010.

摘要

随着信息物理融合系统(Cyber-Physical Systems

CPS)应用的越来越普及

CPS的设计和实现能否满足实际需求显得至关重要.本文提出了一种CPS建模与属性验证框架.在框架中

首先使用HybridUML对CPS进行建模

然后将该通用模型转换为形式化模型

进而进行形式化验证.本文采用的形式化验证方法为dL(Differential Dynamic Logic)

其操作模型为hybrid program.将HybridUML模型转换为hybrid program时

基于语义一致性的原则定义转换规则.转换完成后

结合得到的hybrid program对验证的CPS属性进行规约

最后使用定理证明器KeYmaera对属性进行自动化验证.

Abstract

With the wide application of cyber-physical systems(CPS)

it is of vital importance to ensure that the design and implementation of CPS meet critical performance requirements (e.g.

security

reliability).This paper presents a framework for CPS modeling and verification.In the framework

CPS are modelled by HybridUML and then the generic model is transformed to a formal model that is suitable for reasoning with the help of formal methods.The formal method adopted is differential dynamic logic(dL) whose operational model is hybrid program(HP).When transforming a HybridUML model to its corresponding HP presentation

transformation rules are defined according to semantic consistency.After transformation

CPS properties are specified on the basis of the resulting HP

and finally

the properties are automatically verified through the theorem prover KeYmaera.

关键词

Keywords

references

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于幂表的并行加法器的归纳验证

一种面向嵌入式软件体系结构的形式化建模方法

基于XCFG的BPEL数据流属性分析与验证

双极模拟集成电路计算机辅助剖析和验证系统