Transforming HybridUML to Hybrid Program for CPS Property Verification

ZHU Min; LI Bi-xin; CHEN Qiao-qiao; JI Shun-hui; LI Jia-kai

doi:10.3969/j.issn.0372-2112.2012.06.010

您当前的位置：

首页 >

文章列表页 >

Transforming HybridUML to Hybrid Program for CPS Property Verification

更新时间：2025-07-16

- Transforming HybridUML to Hybrid Program for CPS Property Verification
- Acta Electronica Sinica Vol. 40, Issue 6, Pages: 1126-1132(2012)
- 作者机构：
  
  东南大学计算机科学与工程学院,江苏,南京,211189
- 作者简介：
- 基金信息：
  
  National Natural Science Foundation of China (No.60973149);Doctoral Foundation (No.20100092110022);Open Project of the State Key Laboratory of Computer Science (No.SYSKF1110)
- DOI：10.3969/j.issn.0372-2112.2012.06.010
  CLC： TP301
- Published：2012
- 稿件说明：
移动端阅览
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：

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

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Inductive Verification of Powerlist-Based Carry Lookahead Adders

A Formal Modeling Method for Embedded Software Architecture

XCFG-Based Analysis and Verification for Data Flow Property of BPEL

Bipoar Analog Integrated Circuit Computer Aided Dissection and Verification System

Related Author

任兴田

方娟

侯亚荣

代桂平

王勇

SONG Guo-xin

SHAO Zhi-qing

ZHANG Huan-huan

Related Institution

College of Computer Science & Technology,Beijing University of Technology

College of Electronic Information & Control Engineering,Beijing University of Technology

Institute of Computer Technology,East China University of Science and Technology

Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences

Institute of Computer TechnologyEast China University of Science and TechnologyShanghai 200237China

⁰