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]
Tiwari A.Approximate reachability for linear systems .Proceedings of Hybrid Systems:Computation and Control .Verlag:Springer,2003.514-525.
[3]
Zhou CC,Hansen MR.Duration Calculus:A Formal Approach to Real-Time Systems[M].Heidelberg:Springer,2004.41-62.
[4]
刘亚萍,黄志球,祝义.基于元建模的实时系统模型转换方法研究[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)
[5]
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.
[6]
Platzer,A.Logical Analysis of Hybrid Systems:Proving Theorems for Complex Dynamics[M].Heidelberg:Springer,2010.
[7]
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.
[8]
赖明志,尤晋元.从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)
[9]
Chutinan A,Krogh,BH.Computational techniques for hybrid system verification[J].IEEE Transactions on Automatic Control,2003,48(1):64-75.
[10]
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.
[11]
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.
[12]
Platzer A.Differential dynamic logic for hybrid systems[J].Journal of Automated Reasoning,2008,41(2):143-189.
[13]
Stefan Bisanz.Executable HybridUML Semantics:A Transformation Definition .Bremen:University of Bremen,2005.
[14]
周颖,郑国梁,等.面向模型检验的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)
[15]
Platzer A,Quesel JD.KeYmaera:A hybrid theorem prover for hybrid systems .International Joint Conference on Automated Reasoning(IJCAR) .Heidelberg:Springer,2008.171-178.
[16]
Caplat G,Sourrouille J-L.Model mapping using formalism extensions[J].IEEE Software,2005,22(2):44-51.
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.
