[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. |