混杂系统模型验证工具的验证效果分析
|
摘要
混杂系统的形式验证技术是利用数学分析方法对混杂系统的安全性进行验证。近十年来,模型验证技术是形式验证研究的主要方法。模型验证技术是指,利用计算机强大的计算功能自动地对混杂系统的数学模型进行整个状态空间中进行遍历搜索,对系统所有可能的运行轨迹进行收敛计算或过近似计算,以检验系统的实现方案是否满足系统的设计要求。
论文首先介绍了模型验证的概念和特点,常用的混杂系统建模方法如混杂自动机、混杂Petri网、层次结构和时段演算。分析了可达集的两种计算方法—前向和后向可达集算法,对可达集的过近似方法作了系统的阐述。最后详细介绍了模型验证的国内外研究状况和常用的模型验证工具。
针对混杂系统连续子系统和离散子系统相互作用的特点,研究了混杂自动机模、多面体混杂自动机和混杂I/O自动机的建模方法;对于混杂系统的流管道过近似问题,给出了齐诺多面体(zonotopes)的基于中心点和生成元(generators)的表达式和过近似算法,分析了该算法的保守性、封闭性、集合交并处理能力以及收敛性。通过比较凸多面体过近似和齐诺多面体过近似算法的适用对象、计算方法、过近似保守性和随维数增长的计算复杂度,对两种算法的优劣和特点进行了详细的分析。
针对常压炉加热炉系统(线性混杂系统)和汽车自适应巡航系统(非线性混杂系统)建立数学模型,抽象出验证问题,给出ACTL验证规范。使用PHAVer和CheckMate验证工具分别对上述两种系统建立混杂I/O自动机模型和阈值切换系统模型,应用齐诺多面体流管道过近似方法和凸多面体流管道过近似方法进行模型检验,对系统的状态可达性和运行安全性进行了分析,并给出验证结论。通过上述结论,分析验证工具CheckMate和PHAVer的保守性、消耗时间和内存空间占用率,对上述两种验证工具的验证效果进行了比较。
Hybrid systems formal verification is a mathematically-based technology for specifying the hybrid system’s safety porperty. In recent ten years, model verification technology is the main method of formal verification. Model verification is to verify if a system satisfies the designing requirements by traversal search algorithms using computer to automatically check all states space through and convergently or over-approximately computing possible trajectories.
In this thesis, the conception and characters of modeling verification has been firstly introduced, and then the useful modeling methods such as hybrid automaton, hybrid Petri net, hierarchical structure and duration calculus. The front computing method, backward computing method and over-approximated method for reachable sets have been systematically anglicized. Finally introduce the native and abroad researching status and useful modeling tools.
Due to the character of hybrid system that not only include continuous subsystem and discrete subsystem, investigate the hybrid automaton, polyhedron hybrid automaton and hybrid input and output automaton. For the problem of over-approximated flow pipe, the new over-approximated polyhedron zonotopes which represent the reachable sets based on the center and generators. Analyze the conservative and close property, intersection and convergence. Through comparing adaptive system, computing method and computing complexity, tells the advantages and disadvantages from convex hull and zonotopes.
Build mathematic model, abstract the verification questions, provide the ACTL specification for atmospheric pressure oven heating system (linear system) and automobile adaptive cruise system (nonlinear system). Use PHAVer and CheckMate to construct the hybrid system respectively, apply zonotopes polyhedral and convex hull to over-approximated flow pipe for verifing models, analyzing the state reachability and safety property for the above mentioned hybrid system. Through analyzing the conservative property, time consumption and output file size, comparing the advantages and disadvantages of CheckMate and PHAVer.
论文首先介绍了模型验证的概念和特点,常用的混杂系统建模方法如混杂自动机、混杂Petri网、层次结构和时段演算。分析了可达集的两种计算方法—前向和后向可达集算法,对可达集的过近似方法作了系统的阐述。最后详细介绍了模型验证的国内外研究状况和常用的模型验证工具。
针对混杂系统连续子系统和离散子系统相互作用的特点,研究了混杂自动机模、多面体混杂自动机和混杂I/O自动机的建模方法;对于混杂系统的流管道过近似问题,给出了齐诺多面体(zonotopes)的基于中心点和生成元(generators)的表达式和过近似算法,分析了该算法的保守性、封闭性、集合交并处理能力以及收敛性。通过比较凸多面体过近似和齐诺多面体过近似算法的适用对象、计算方法、过近似保守性和随维数增长的计算复杂度,对两种算法的优劣和特点进行了详细的分析。
针对常压炉加热炉系统(线性混杂系统)和汽车自适应巡航系统(非线性混杂系统)建立数学模型,抽象出验证问题,给出ACTL验证规范。使用PHAVer和CheckMate验证工具分别对上述两种系统建立混杂I/O自动机模型和阈值切换系统模型,应用齐诺多面体流管道过近似方法和凸多面体流管道过近似方法进行模型检验,对系统的状态可达性和运行安全性进行了分析,并给出验证结论。通过上述结论,分析验证工具CheckMate和PHAVer的保守性、消耗时间和内存空间占用率,对上述两种验证工具的验证效果进行了比较。
Hybrid systems formal verification is a mathematically-based technology for specifying the hybrid system’s safety porperty. In recent ten years, model verification technology is the main method of formal verification. Model verification is to verify if a system satisfies the designing requirements by traversal search algorithms using computer to automatically check all states space through and convergently or over-approximately computing possible trajectories.
In this thesis, the conception and characters of modeling verification has been firstly introduced, and then the useful modeling methods such as hybrid automaton, hybrid Petri net, hierarchical structure and duration calculus. The front computing method, backward computing method and over-approximated method for reachable sets have been systematically anglicized. Finally introduce the native and abroad researching status and useful modeling tools.
Due to the character of hybrid system that not only include continuous subsystem and discrete subsystem, investigate the hybrid automaton, polyhedron hybrid automaton and hybrid input and output automaton. For the problem of over-approximated flow pipe, the new over-approximated polyhedron zonotopes which represent the reachable sets based on the center and generators. Analyze the conservative and close property, intersection and convergence. Through comparing adaptive system, computing method and computing complexity, tells the advantages and disadvantages from convex hull and zonotopes.
Build mathematic model, abstract the verification questions, provide the ACTL specification for atmospheric pressure oven heating system (linear system) and automobile adaptive cruise system (nonlinear system). Use PHAVer and CheckMate to construct the hybrid system respectively, apply zonotopes polyhedral and convex hull to over-approximated flow pipe for verifing models, analyzing the state reachability and safety property for the above mentioned hybrid system. Through analyzing the conservative property, time consumption and output file size, comparing the advantages and disadvantages of CheckMate and PHAVer.
引文
[1]方敏,张雅顺,李辉.混合系统的形式验证方法[J].系统仿真学报,2006(10):2921-2924.
[2] H.S.Witsenhausen. A class of hybrid-state continuous-time dynamic systems. [J]. IEEE Transaction on Automatic Control, 1966, 11(6):665-683.
[3] R. Alur, C. Courcoubetis, T. Henzinger, and P.–H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. [C]. In R. Grossman, A. Nerode, A. Ravn, and H. Rischel, editors, Hybrid System, Lecture Notes in Computer Science 739, Springer-Verlag, 1993, pages 209-299.
[4] Chutinan A. Hybrid system verification using discrete model approximations [D]. PhD thesis, Electrical and Computer Engineering Department, Carnegie Mellon University, Pittsburgh, USA, 1999.
[5] Henzinger, T.A.: The theory of hybrid automata [C]. In: Proc. 11th Annual IEEESymposium on Logic inComputer Science, LICS’96, New Brunswick, New Jersey, 27–30 July 1996, pp. IEEE Computer Society Press 1996, 278-292.
[6] Gue′guen, H., & Zaytoon, J. On the formal verification of hybrid systems [J]. Control Engineering Practice, 2004, 12(10), 1253-1268.
[7] Frehse, G., Krogh, B.H., Rutenbar, R.A.: Verifying analog oscillator circuits using forward/backward refinement [J]. In: ACMSIGDA, Munich, Germany Proc. Conf. on Design, Automation and Test in Europe 2006, DATE 06.
[8] J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation [M]. Addison-Wesley, 1979.
[9] Henzinger T A, Ho P H, Wong-Toi H.: HYTECH: a model checker for hybrid systems [J]. Int. J. Softw. Tools Technol. Transfer1 (1–2), 1997, page 110–122.
[10] Alur.R., Henzinger, T.A., Ho, P.-H.: Automatic symbolic verification of embedded systems [J]. IEEE Trans. Softw. Eng.22, 1996, page 181-201
[11] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P., Nicollin. The algorithmic analysis of hybrid systems [J]. Theoretical Computer Science, 1995, 138, 3–34.
[12] Chutinan, A. and Krogh B.H. Computing polyhedral approximating automata for a class of linear hybrid systems. In Hybrid Systems V, [C].Lecture Notes in Computer Science. Springer-Verlag, 1998.
[13] Lynch, N.A., Segala R., Vandrager, F.W.L. Hybrid I/O automata. [J]. Informat.Comput. 2003, 185(1), 105-157.
[14] Fresh,G: Compositional verification of hybrid systems using simulation relations [D]. phD thesis, Radboud University Nijmegen,2005.
[15] J. Le Bail, H. Alla, and R. David. Hybrid Petri nets [C]. In Proceedings of 1st European Control Conference, Grenoble, 1991, pages 1472–1477.
[16] FEBBRARO A D, GIUA A, MENGA G. Special issue on hybrid Petri nets [J]. Discrete Event Dynamical Systems: Theory and Applications, 2001, 11(1-2): 5-8.
[17] G. Ciardo, D. Nicol, K.S. Trivedi, "Discrete-event simulation of fluid stochastic Petri Nets [C]. Proc. of Conf. on Petri Nets and Performances Evaluation (Saint Malo, France), 1997, June: 217-25.
[18] Febbraro A D,Giua A,Menga G.Special issue on hybrid Petri nets [J]. Discrete Event Dynamical Systems:Theory and Applications,2001,11(1-2):5-8.
[19] Champagnat R,Esteban P,Pingaud H,et a1.Petri net based modeling of hybrid systems [J]. Computers in Industry , 1998, 36(1-2): 139-146.
[20] Giua A , Usai E . Modeling hybrid systems by high—level Petri nets [J].European J of Automation APII—JESA,1998,32(9-10):1209-1231.
[21] Caradec M,Prunet F.Modeling of hybrid flexible production systems by colored batches Petri nets [J].European J of Automation APII—JESA, 1998, 32 9-10):1255-1269.
[22] Grossman R L, Nerode A, Ravn A P, et al. Hybrid System——Lecture Notes in Computer Science [M]. Berlin: Springer-Verlag, 1993.
[23] HansenM,Zhou Cbaohen.Semantics and completeness of duration calculus Bakker de J,Huizing C,Roever de W ,Rozenberg G eds [J]. Real-Time: Theory in Practice.REX Workshop.1992, LNCS 600, pp209-225.
[24] Skakkebmk J, Ravn A, Ruschel H, Zhou Chaochen Specification of embedded real-time systems.In:Proc 4th Euromicro Workshop Real-Time Systems,IEEE Press, l992,116-121.
[25] Skakkeb?k J.U. and Sestoft P.:Checking Validity of Duration Calculus Formulas [R]. ProCoS II, ESPRIT BRA 7071, report no. ID/DTH JUS 3/1, Department of Computer Science, Technical University of Denmark, 1994.
[26] Ravn A, Rischel A, Hansen K. Specifying and verifying requirements of real-time Systems [C]. In: The proceedings of the ACM SIGSOFT’91 Conference on software for Critical Systems, New Orleans, December 4-6, 1991, ACM Software Engineering Notes,1991, 15 (5): 44-54.
[27] M. Broucke, M. D. Di Benedetto, S. Di Gennaro, and A.Sangiovanni-Vincentelli, Optimal Control Using Bisimulations: Implementation [J]. Hybrid System: Computation and Control. LNCS Vol. 2034, Springer-Verlag, 2001, 175-188.
[28] J. Aubin, Viability Theory [M]. Systems & Contorl: Foundations & Applications, Birkhauser,1991.
[29] J. Aubin, J. Lygeros, M. Quincampoix, S. Sastry and N. Seube, Impulse Differential Inclusions: a Viability Approach to Hybrid Systems [J], IEEE Transition on Automatic Control, 2002. 47(1): 2-20.
[30] Claire J. Tomlin, Ian Mitchell, Alexandre M. Bayen, and Meeko Oishi, Computational Techniques for the Verification of Hybrid Systems [J]. Proceedings of the IEEE, 2000, vol. 88, No.7.
[31] Bournez K., Maler O., Pnueli A., Orthogonal Polyhedra: Represntation and Computation [C]. Hybrid System: Computation and Control. 1999, LNCS Vol.1596, Springer, 46-60.
[32] Botchkarev O., Tripakis S., Verification of Hybrid Systems with Linear Differential Inclusions Using Ellipsoidal Approximations [C]. Hybrid Systems: Computation and Control.2000, LNCS Vol.1790, Springer, 73-88.
[33] Kurzhanski A., varaiya P., Ellipsiodal Techniques for Rechability Analysis [C]. Hybrid Systems: Computational and Control.2000, LNCS Vol. 1790, Springer, 202-214.
[34] Green Street M., R. Mitchell I., Reachability Analysis Using Polygonal Projections [C]. Hybrid Systems: Computational and Control. LNCS Vol. 1790, Springer, 202-214.
[35] Chutinan A., Krough B., Verification of Infinite-State Dynamic Systems Using Approximate Quotient Transition systems [J]. IEEE Transaction on Automatic Control. 2001, 46: 1401-1410.
[36] Bernard Chazelle, An Optimal Convex Hull Algorithm in any Fixed Dimension [J]. Discrete and Computational Geometry, 199.,10:377-409.
[37] Avis D., Bremner D., Bremner D., Seidel R., How Good are Convex Hull Algorithms [J]. Computational Geometry: Theory and Applications, 1997, 7:265-301.
[38] Puri A., Borkar V., Varaiya P.,ε-approximations of Differential Inclusions. Hybrid SystemⅢ[C]. 1996, LNCS Springer Vol.1066.
[39] Stursberg O., Analysis of Switched Continuous Systems Based on Discrete Mixed Processes.2000, 73-78.
[40] Esposito J E. Randomized Test Case Generation for Hybrid Systems: MetricSelection[A]. Proceedings of the Annual Southeastern Symposium on system Theory[C], 2004: 236-240.
[41] Berard B., M. Bidoit, A. Finkel, et al. Systems and software verification: model-checking techniques and tools [M]. Berlin: Springer, 2001.
[42] Henzinger, T.A., Ho, P.-H., Wong-Toi. H.: HYTECH: a model checker for hybrid sytems [J]. Int. J. Softw. Tools Technol. TransferⅠ(1-2)
[43] Frehse G. Phaver: Algorithmic verification of hybrid systems past hytech [C]. M. Morari and L. Thiele, editors, Hybrid Systems: Computation and Control (HSCC’05), Zurich, CH, 2005: Mar. 9–11.
[44] Emerson E A and Clarke E M. Using Branching Time Temporal Logic to Synthesize Synchronization. Science of Computer Programming[J], 1982, 2(3):241-266
[45] Queille J P and Sifakis J. Specification and Verification of Concurrent Systems in CESAR[A]. Proceedings of the 5th Colloquium on International Symposium on Program[C], 1982: 337-351
[46] Bryant R E. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams[J]. ACM Computing Surveys, 1992, 24(3): 293-318.
[47] Chutinan, A., Krogh. B. Computation techniques for hybrid systems verification [J]. IEEE Transactions on Automatic Control, 2003, 48, 64-75.
[48] Fehnker A., Clarke E., Jha S., Krogh B. Refining abstractions of hybrid systems using counterexample fragments. In M. Morari & L Thiele(Eds.). Hybrid systems: Computation and control: 8th international workshop, 2005, 242-257.
[49] Frehse G, Krogh B H, Rutenbar R A. Verifying analog oscillator circuits using forward/backward refinement [C]//Proc. Conf. on Design, Automation and Test in Europe (DATE 06). ACMSIGDA, Munich, Germany, 2006: Mar. 6-10.
[50] Ramdani N., Meslem N., Candau Y. Reachability analysis of uncertain nonlinear systems using guaranted set integration[C]. IFACWorld congress, Seoul IFAC, 2008.
[52] Hermenegildo, M V, Puebla G. Possibly not closed convex polyhedra and the Parma Polyhedra Library [C]. Static Analysis: Proc. of the 9th Int. Symposium. LNCS, Springer, Madrid, Spain, 2002, 2477: 213–229.
[52] Asarin E., Dang T. Abstraction by projection and application to multi-affine systems [C]. Hybrid systems: Computation and control: 7th international workshop,32-47.
[53] Han Z., Krogh B. Reachability analysis for affine systems using ?-De composition [C]. ECC CDC 2005, IEEE-EUCS.
[54] Han Z., Krogh B. Reachability analysis of large-scale affine systems using low-dimensional polytopes. Hybrid Systems: Computation and control: 9th international workshop, 287-301.
[55] Girard A., Julius A., Pappas G. Approximate simulation relations for hybrid systems[C]. 2nd IFAC conference on anlysis on design of hybrid system ADHS06, 2006, 106-111.
[56] Asarin E., Dang T., Girard A. Reachability analysis of non-linear systems using conservative approximation[C]. HSCC2003, springer, 20-35.
[57]萧德云,莫以为.混合动态系统及其应用综述[J].控制理论与应用,Vol.19,No.1 pp 1-8.
[58] Witsenhausen H S. a class of hybrid-state continuous-time dynamic systems[J]. IEEE Transactions on Automatic Control, 1996, 11(6): 665-683
[59] Molnar, Levente, Veres. Sandor M System verification of autonomous underwater vehicles by model checking [C]. European Control Conference (ECC’09), Budapest, Hungary, 2009: Aug. 23-26.
[60]李辉,方敏.基于流管道过近似的混合系统形式化验证技术[J].合肥工业大学学报(自然科学版),2008,31(01): 51-55.
[61] Kuhn W. Zonotopes dynamics in numerical quality control[J]. Mathmeatical Visualization, 1998, springer, 125-134. C.J. Tomlin, I. Mitchell, A.M. Bayen, and M. Oishi. Computational Techniques for the Verification of Hybrid Systems[A]. Proceedings of the IEEE[C], 2003. 986-1001.
[62] A. Chutinan, B.H. Krogh, Verification of polyhedral invariant hybrid automata using polygonal flow pipe approximations. Hybrid Systems: Computation and Control, F. Vaandrager, J van Schuppen(Eds), no.1569 in LNCS, 1999, Springer, 76-90.
[63] Lafferriere G, Pappas G J, Sastry S. Hybrid systems with finite bisimulations[R]. Technical Report UCB/ERL M98/15, University of California at Berkeley, April 1998.
[64]张苗苗.混合系统的离散模型近似及形式验证[D].上海交通大学博士学位论文, 2000.12.
[65] S. P etersson,Analysis and Design of Hybrid Systems[D]. Ph.D.D issertation, Chalmers University of Technology ,June,1999.
[66] M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time[J]. Acta Informatica 20(1983):207-226.
[67] Clarke E M, Grumberg Jr O, Peled D A. Model Checking[M], Cambridge, Massachusetts: The MIT Press, 1999.
[68] J Hespanha, A. Tiwari. Fixed Point Iteration for Computing the Time Elapse Operator [C]// HSCC 2006, LNCS, 2006, 3927: 537–551.
[69]孙玉良,闵祥禄.常减压蒸馏装置安全运行与管理[M].北京:中国石化出版社,2006:39-42
[70] Girard, A.R., J.B. Souza, J.A. Misenser and J.K. J.K. Hedrick: Acontrol architecture for integrated cooperative cruise control and collision warning systems [C].Proc. 40th IEEE Conf. on Decision and Control.
[2] H.S.Witsenhausen. A class of hybrid-state continuous-time dynamic systems. [J]. IEEE Transaction on Automatic Control, 1966, 11(6):665-683.
[3] R. Alur, C. Courcoubetis, T. Henzinger, and P.–H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. [C]. In R. Grossman, A. Nerode, A. Ravn, and H. Rischel, editors, Hybrid System, Lecture Notes in Computer Science 739, Springer-Verlag, 1993, pages 209-299.
[4] Chutinan A. Hybrid system verification using discrete model approximations [D]. PhD thesis, Electrical and Computer Engineering Department, Carnegie Mellon University, Pittsburgh, USA, 1999.
[5] Henzinger, T.A.: The theory of hybrid automata [C]. In: Proc. 11th Annual IEEESymposium on Logic inComputer Science, LICS’96, New Brunswick, New Jersey, 27–30 July 1996, pp. IEEE Computer Society Press 1996, 278-292.
[6] Gue′guen, H., & Zaytoon, J. On the formal verification of hybrid systems [J]. Control Engineering Practice, 2004, 12(10), 1253-1268.
[7] Frehse, G., Krogh, B.H., Rutenbar, R.A.: Verifying analog oscillator circuits using forward/backward refinement [J]. In: ACMSIGDA, Munich, Germany Proc. Conf. on Design, Automation and Test in Europe 2006, DATE 06.
[8] J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation [M]. Addison-Wesley, 1979.
[9] Henzinger T A, Ho P H, Wong-Toi H.: HYTECH: a model checker for hybrid systems [J]. Int. J. Softw. Tools Technol. Transfer1 (1–2), 1997, page 110–122.
[10] Alur.R., Henzinger, T.A., Ho, P.-H.: Automatic symbolic verification of embedded systems [J]. IEEE Trans. Softw. Eng.22, 1996, page 181-201
[11] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P., Nicollin. The algorithmic analysis of hybrid systems [J]. Theoretical Computer Science, 1995, 138, 3–34.
[12] Chutinan, A. and Krogh B.H. Computing polyhedral approximating automata for a class of linear hybrid systems. In Hybrid Systems V, [C].Lecture Notes in Computer Science. Springer-Verlag, 1998.
[13] Lynch, N.A., Segala R., Vandrager, F.W.L. Hybrid I/O automata. [J]. Informat.Comput. 2003, 185(1), 105-157.
[14] Fresh,G: Compositional verification of hybrid systems using simulation relations [D]. phD thesis, Radboud University Nijmegen,2005.
[15] J. Le Bail, H. Alla, and R. David. Hybrid Petri nets [C]. In Proceedings of 1st European Control Conference, Grenoble, 1991, pages 1472–1477.
[16] FEBBRARO A D, GIUA A, MENGA G. Special issue on hybrid Petri nets [J]. Discrete Event Dynamical Systems: Theory and Applications, 2001, 11(1-2): 5-8.
[17] G. Ciardo, D. Nicol, K.S. Trivedi, "Discrete-event simulation of fluid stochastic Petri Nets [C]. Proc. of Conf. on Petri Nets and Performances Evaluation (Saint Malo, France), 1997, June: 217-25.
[18] Febbraro A D,Giua A,Menga G.Special issue on hybrid Petri nets [J]. Discrete Event Dynamical Systems:Theory and Applications,2001,11(1-2):5-8.
[19] Champagnat R,Esteban P,Pingaud H,et a1.Petri net based modeling of hybrid systems [J]. Computers in Industry , 1998, 36(1-2): 139-146.
[20] Giua A , Usai E . Modeling hybrid systems by high—level Petri nets [J].European J of Automation APII—JESA,1998,32(9-10):1209-1231.
[21] Caradec M,Prunet F.Modeling of hybrid flexible production systems by colored batches Petri nets [J].European J of Automation APII—JESA, 1998, 32 9-10):1255-1269.
[22] Grossman R L, Nerode A, Ravn A P, et al. Hybrid System——Lecture Notes in Computer Science [M]. Berlin: Springer-Verlag, 1993.
[23] HansenM,Zhou Cbaohen.Semantics and completeness of duration calculus Bakker de J,Huizing C,Roever de W ,Rozenberg G eds [J]. Real-Time: Theory in Practice.REX Workshop.1992, LNCS 600, pp209-225.
[24] Skakkebmk J, Ravn A, Ruschel H, Zhou Chaochen Specification of embedded real-time systems.In:Proc 4th Euromicro Workshop Real-Time Systems,IEEE Press, l992,116-121.
[25] Skakkeb?k J.U. and Sestoft P.:Checking Validity of Duration Calculus Formulas [R]. ProCoS II, ESPRIT BRA 7071, report no. ID/DTH JUS 3/1, Department of Computer Science, Technical University of Denmark, 1994.
[26] Ravn A, Rischel A, Hansen K. Specifying and verifying requirements of real-time Systems [C]. In: The proceedings of the ACM SIGSOFT’91 Conference on software for Critical Systems, New Orleans, December 4-6, 1991, ACM Software Engineering Notes,1991, 15 (5): 44-54.
[27] M. Broucke, M. D. Di Benedetto, S. Di Gennaro, and A.Sangiovanni-Vincentelli, Optimal Control Using Bisimulations: Implementation [J]. Hybrid System: Computation and Control. LNCS Vol. 2034, Springer-Verlag, 2001, 175-188.
[28] J. Aubin, Viability Theory [M]. Systems & Contorl: Foundations & Applications, Birkhauser,1991.
[29] J. Aubin, J. Lygeros, M. Quincampoix, S. Sastry and N. Seube, Impulse Differential Inclusions: a Viability Approach to Hybrid Systems [J], IEEE Transition on Automatic Control, 2002. 47(1): 2-20.
[30] Claire J. Tomlin, Ian Mitchell, Alexandre M. Bayen, and Meeko Oishi, Computational Techniques for the Verification of Hybrid Systems [J]. Proceedings of the IEEE, 2000, vol. 88, No.7.
[31] Bournez K., Maler O., Pnueli A., Orthogonal Polyhedra: Represntation and Computation [C]. Hybrid System: Computation and Control. 1999, LNCS Vol.1596, Springer, 46-60.
[32] Botchkarev O., Tripakis S., Verification of Hybrid Systems with Linear Differential Inclusions Using Ellipsoidal Approximations [C]. Hybrid Systems: Computation and Control.2000, LNCS Vol.1790, Springer, 73-88.
[33] Kurzhanski A., varaiya P., Ellipsiodal Techniques for Rechability Analysis [C]. Hybrid Systems: Computational and Control.2000, LNCS Vol. 1790, Springer, 202-214.
[34] Green Street M., R. Mitchell I., Reachability Analysis Using Polygonal Projections [C]. Hybrid Systems: Computational and Control. LNCS Vol. 1790, Springer, 202-214.
[35] Chutinan A., Krough B., Verification of Infinite-State Dynamic Systems Using Approximate Quotient Transition systems [J]. IEEE Transaction on Automatic Control. 2001, 46: 1401-1410.
[36] Bernard Chazelle, An Optimal Convex Hull Algorithm in any Fixed Dimension [J]. Discrete and Computational Geometry, 199.,10:377-409.
[37] Avis D., Bremner D., Bremner D., Seidel R., How Good are Convex Hull Algorithms [J]. Computational Geometry: Theory and Applications, 1997, 7:265-301.
[38] Puri A., Borkar V., Varaiya P.,ε-approximations of Differential Inclusions. Hybrid SystemⅢ[C]. 1996, LNCS Springer Vol.1066.
[39] Stursberg O., Analysis of Switched Continuous Systems Based on Discrete Mixed Processes.2000, 73-78.
[40] Esposito J E. Randomized Test Case Generation for Hybrid Systems: MetricSelection[A]. Proceedings of the Annual Southeastern Symposium on system Theory[C], 2004: 236-240.
[41] Berard B., M. Bidoit, A. Finkel, et al. Systems and software verification: model-checking techniques and tools [M]. Berlin: Springer, 2001.
[42] Henzinger, T.A., Ho, P.-H., Wong-Toi. H.: HYTECH: a model checker for hybrid sytems [J]. Int. J. Softw. Tools Technol. TransferⅠ(1-2)
[43] Frehse G. Phaver: Algorithmic verification of hybrid systems past hytech [C]. M. Morari and L. Thiele, editors, Hybrid Systems: Computation and Control (HSCC’05), Zurich, CH, 2005: Mar. 9–11.
[44] Emerson E A and Clarke E M. Using Branching Time Temporal Logic to Synthesize Synchronization. Science of Computer Programming[J], 1982, 2(3):241-266
[45] Queille J P and Sifakis J. Specification and Verification of Concurrent Systems in CESAR[A]. Proceedings of the 5th Colloquium on International Symposium on Program[C], 1982: 337-351
[46] Bryant R E. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams[J]. ACM Computing Surveys, 1992, 24(3): 293-318.
[47] Chutinan, A., Krogh. B. Computation techniques for hybrid systems verification [J]. IEEE Transactions on Automatic Control, 2003, 48, 64-75.
[48] Fehnker A., Clarke E., Jha S., Krogh B. Refining abstractions of hybrid systems using counterexample fragments. In M. Morari & L Thiele(Eds.). Hybrid systems: Computation and control: 8th international workshop, 2005, 242-257.
[49] Frehse G, Krogh B H, Rutenbar R A. Verifying analog oscillator circuits using forward/backward refinement [C]//Proc. Conf. on Design, Automation and Test in Europe (DATE 06). ACMSIGDA, Munich, Germany, 2006: Mar. 6-10.
[50] Ramdani N., Meslem N., Candau Y. Reachability analysis of uncertain nonlinear systems using guaranted set integration[C]. IFACWorld congress, Seoul IFAC, 2008.
[52] Hermenegildo, M V, Puebla G. Possibly not closed convex polyhedra and the Parma Polyhedra Library [C]. Static Analysis: Proc. of the 9th Int. Symposium. LNCS, Springer, Madrid, Spain, 2002, 2477: 213–229.
[52] Asarin E., Dang T. Abstraction by projection and application to multi-affine systems [C]. Hybrid systems: Computation and control: 7th international workshop,32-47.
[53] Han Z., Krogh B. Reachability analysis for affine systems using ?-De composition [C]. ECC CDC 2005, IEEE-EUCS.
[54] Han Z., Krogh B. Reachability analysis of large-scale affine systems using low-dimensional polytopes. Hybrid Systems: Computation and control: 9th international workshop, 287-301.
[55] Girard A., Julius A., Pappas G. Approximate simulation relations for hybrid systems[C]. 2nd IFAC conference on anlysis on design of hybrid system ADHS06, 2006, 106-111.
[56] Asarin E., Dang T., Girard A. Reachability analysis of non-linear systems using conservative approximation[C]. HSCC2003, springer, 20-35.
[57]萧德云,莫以为.混合动态系统及其应用综述[J].控制理论与应用,Vol.19,No.1 pp 1-8.
[58] Witsenhausen H S. a class of hybrid-state continuous-time dynamic systems[J]. IEEE Transactions on Automatic Control, 1996, 11(6): 665-683
[59] Molnar, Levente, Veres. Sandor M System verification of autonomous underwater vehicles by model checking [C]. European Control Conference (ECC’09), Budapest, Hungary, 2009: Aug. 23-26.
[60]李辉,方敏.基于流管道过近似的混合系统形式化验证技术[J].合肥工业大学学报(自然科学版),2008,31(01): 51-55.
[61] Kuhn W. Zonotopes dynamics in numerical quality control[J]. Mathmeatical Visualization, 1998, springer, 125-134. C.J. Tomlin, I. Mitchell, A.M. Bayen, and M. Oishi. Computational Techniques for the Verification of Hybrid Systems[A]. Proceedings of the IEEE[C], 2003. 986-1001.
[62] A. Chutinan, B.H. Krogh, Verification of polyhedral invariant hybrid automata using polygonal flow pipe approximations. Hybrid Systems: Computation and Control, F. Vaandrager, J van Schuppen(Eds), no.1569 in LNCS, 1999, Springer, 76-90.
[63] Lafferriere G, Pappas G J, Sastry S. Hybrid systems with finite bisimulations[R]. Technical Report UCB/ERL M98/15, University of California at Berkeley, April 1998.
[64]张苗苗.混合系统的离散模型近似及形式验证[D].上海交通大学博士学位论文, 2000.12.
[65] S. P etersson,Analysis and Design of Hybrid Systems[D]. Ph.D.D issertation, Chalmers University of Technology ,June,1999.
[66] M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time[J]. Acta Informatica 20(1983):207-226.
[67] Clarke E M, Grumberg Jr O, Peled D A. Model Checking[M], Cambridge, Massachusetts: The MIT Press, 1999.
[68] J Hespanha, A. Tiwari. Fixed Point Iteration for Computing the Time Elapse Operator [C]// HSCC 2006, LNCS, 2006, 3927: 537–551.
[69]孙玉良,闵祥禄.常减压蒸馏装置安全运行与管理[M].北京:中国石化出版社,2006:39-42
[70] Girard, A.R., J.B. Souza, J.A. Misenser and J.K. J.K. Hedrick: Acontrol architecture for integrated cooperative cruise control and collision warning systems [C].Proc. 40th IEEE Conf. on Decision and Control.