随着信息物理融合系统(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.
关键词
信息物理融合系统 /
微分动态逻辑 /
HybridUML /
模型转换 /
验证
{{custom_keyword}} /
Key words
CPS /
differential dynamic logic /
HybridUML /
model transformation /
verification
{{custom_keyword}} /
中图分类号:
TP301
{{custom_clc.code}}
({{custom_clc.text}})
{{custom_sec.title}}
{{custom_sec.title}}
{{custom_sec.content}}
参考文献
[1] Lee EA.Cyber physical systems:Design challenges .Proceedings of 11th IEEE Symposium on Object Oriented Real-time Distributed Computing(ISORC) .Washington:IEEE Computer Society,2008.363-369.
[2] Chutinan A,Krogh,BH.Computational techniques for hybrid system verification[J].IEEE Transactions on Automatic Control,2003,48(1):64-75.
[3] Tiwari A.Approximate reachability for linear systems .Proceedings of Hybrid Systems:Computation and Control .Verlag:Springer,2003.514-525.
[4] Platzer A,Clarke,EM.The image computation problem in hybrid systems model checking .10workshop on Hybrid System:Computation and control .Heidelberg:Springer,2007.473-486.
[5] Collins P,Lygeros J.Computability of finite-time reachable sets for hybrid systems .Proceedings of the 44th IEEE Conference on Decision and Control,and the European Control Conference .New Jersey:Piscataway,2005.4688-4693.
[6] Zhou CC,Hansen MR.Duration Calculus:A Formal Approach to Real-Time Systems[M].Heidelberg:Springer,2004.41-62.
[7] Platzer A.Differential dynamic logic for hybrid systems[J].Journal of Automated Reasoning,2008,41(2):143-189.
[8] 刘亚萍,黄志球,祝义.基于元建模的实时系统模型转换方法研究[J].小型微型计算机系统,2010,31(11):2146-2153. Liu Yaping,Huang Zhiqiu,Zhu Yi.Research on model transformation method of real-time system based on metamodeling[J].Journal of Chinese Computer Systems,2010,31(11):2146-2153.(in Chinese)
[9] Stefan Bisanz.Executable HybridUML Semantics:A Transformation Definition .Bremen:University of Bremen,2005.
[10] Kirsten Berkenkøtter,Stefan Bisanz,Ulrich Hannemann,Jan Peleska.The HybridUML profile for UML 2.0[J].International Journal on Software Tools for Technology Transfer(STTT),2006,8(2):167-176.
[11] 周颖,郑国梁,等.面向模型检验的UML状态机语义[J].电子学报,2004,51(12):2091-2095. ZHOU Ying,ZHENG Guo-liang,et al.An operational semantics for UML State Machines in model checking context[J].Acta Electronica Sinica,2004,51(12):2091-2095.(in Chinese)
[12] Platzer A,Quesel JD.KeYmaera:A hybrid theorem prover for hybrid systems .International Joint Conference on Automated Reasoning(IJCAR) .Heidelberg:Springer,2008.171-178.
[13] Platzer,A.Logical Analysis of Hybrid Systems:Proving Theorems for Complex Dynamics[M].Heidelberg:Springer,2010.
[14] Caplat G,Sourrouille J-L.Model mapping using formalism extensions[J].IEEE Software,2005,22(2):44-51.
[15] Czarnecki K,Helsen S.Classification of model transformation approaches .OOPSLA’03 Workshop on Generative Techniques in the Context of Model-driven Architecture .New York:ACM Press,2003.
[16] 战德臣,冯锦丹,等.ICEMDA:一种可互操作可配置可执行的模型驱动体系结构[J].电子学报,2008,36(12A):120-127. ZHAN De-chen,FENG Jin-dan,et al.ICEMDA:An interoperable configurable executable model driven architecture[J].Acta Electronica Sinica,2008,36(12A):120-127.(in Chinese)
[17] 赖明志,尤晋元.从UML状态图到PVS规范的自动转换、验证[J].电子学报,2002,30(12A):2122-2125. LAI Ming-zhi,YOU Jin-yuan.Automatic transform UML statechart into PVS[J].Acta Electronica Sinica,2002,30(12A):2122-2125.(in Chinese)
[18] Platzer A,Quesel,J.D.European Train Control System:A case study in formal verification .Formal Methods and Software Engineering:11th International Conference on For- mal Engineering Methods .Heidelberg:Springer,2009.246-265.
{{custom_fnGroup.title_cn}}
脚注
{{custom_fn.content}}
基金
国家自然科学基金 (No.60973149); 博士点基金 (No.20100092110022); 中科院计算机科学国家重点实验室开放基金基金 (No.SYSKF1110)
{{custom_fund}}