线性混合系统的验证方法及其应用
|
摘要
混合系统主要研究由连续性子系统和离散性子系统相互作用而构成的一类动态系统。连续性子系统和离散性子系统二者相互作用,使系统的运行轨迹整体上呈现离散状态的迁移,局部上呈现连续状态渐进演化,表现出更加复杂的动态行为,这就给混合系统运行的安全性和状态的可达性分析带来了困难。
本文的工作是围绕线性混合系统的形式化验证展开的。线性系统具有初始区域为凸多面体且可达集仍为凸多面体的特性。混合系统不变集内的子系统为线性系统,因此可应用线性系统的特性对线性混合系统的形式验证过程进行简化。本文以炼油厂常减压装置中的常压炉加热系统为线性混合系统的例子,分别应用基于流管道和基于简化流管道的形式验证方法进行验证,为线性混合系统的形式验证提供参考。
主要工作包括:
1、研究了基于流管道理论的验证方法,包括:初始状态区域划分、流管道的过近似,商迁移系统迁移关系的确定。
2、对目前主要的验证工具进行了比较,并详细分析了基于流管道理论的验证工具CheckMate各模块的功能。
3、在详细分析了常压炉加热系统工作原理的基础上,建立动态模型,抽象其验证问题;建立混合自动机模型,应用基于流管道的形式验证方法对系统的状态可达性和运行安全性进行分析,得出验证结论;分析了在验证过程中采用不同步长对验证结果的影响。
4、应用基于简化流管道的形式验证方法,对原油加热过程进行验证,对验证结果进行分析。并与基于流管道的形式验证方法得到的验证结果相比较,讨论了两种验证方法的计算复杂度和保守性问题。
Hybrid systems are a class of complex dynamic systems composed by linear subsystem and discrete subsystem which are interacted with each other. Linear and discrete subsystem are interacted, the system's function track was discrete state transition holistically, the stepwise evolvement of linear state is presented partly ,the much complex dynamic action was appeared ,it is very difficult that analysis of the hybrid systems function's security and state's reachability.
All tasks were worked for linear hybrid system formal verification. Linear system has the characteristic that its reachable set is convex hull if its initial region is convex hull. The subsystem is linear system in the hybrid system`s invariable set.The linear hybrid system verification process can be simplified.This thesis used crude oil heat process as example, it was modelled, the system was verified by the formal verification technique based on flow pipe and simplified flow pipe, the system's security and reachability was analyzed,this provided a reference for linear hybrid system verification.
The main work in this thesis is as follows:
1. The verification method based on flow pipe is analyzed, includes: the necessary of partition was analyzed, over approximate flow pipe, the relationship of over approximate flow pipe and quotient transition systems' establishment was analyzed.
2. The verification tools were compared. CheckMate was a verification tool based on flow pipe, its function models was introduced in detail.
3. The crude oil heater process run principle is analyzed,based on that the dynamical model is built,the verification problem is abstracted; hybrid automata model is established, the system`s state reachablity and function security is analyzed used the verification method based on flow pipe, verification result is worked out. The influence on the verification result used the different step in the verification process.
4. The crude oil heat process was verified by the verification method based on simplified flow pipe, The verification result was presented and analyzed. There is a compare between the verification results, they were presented by verification method based on flow pipe and simplified flow pipe. Their conservatism and computation costs were analyzed.
本文的工作是围绕线性混合系统的形式化验证展开的。线性系统具有初始区域为凸多面体且可达集仍为凸多面体的特性。混合系统不变集内的子系统为线性系统,因此可应用线性系统的特性对线性混合系统的形式验证过程进行简化。本文以炼油厂常减压装置中的常压炉加热系统为线性混合系统的例子,分别应用基于流管道和基于简化流管道的形式验证方法进行验证,为线性混合系统的形式验证提供参考。
主要工作包括:
1、研究了基于流管道理论的验证方法,包括:初始状态区域划分、流管道的过近似,商迁移系统迁移关系的确定。
2、对目前主要的验证工具进行了比较,并详细分析了基于流管道理论的验证工具CheckMate各模块的功能。
3、在详细分析了常压炉加热系统工作原理的基础上,建立动态模型,抽象其验证问题;建立混合自动机模型,应用基于流管道的形式验证方法对系统的状态可达性和运行安全性进行分析,得出验证结论;分析了在验证过程中采用不同步长对验证结果的影响。
4、应用基于简化流管道的形式验证方法,对原油加热过程进行验证,对验证结果进行分析。并与基于流管道的形式验证方法得到的验证结果相比较,讨论了两种验证方法的计算复杂度和保守性问题。
Hybrid systems are a class of complex dynamic systems composed by linear subsystem and discrete subsystem which are interacted with each other. Linear and discrete subsystem are interacted, the system's function track was discrete state transition holistically, the stepwise evolvement of linear state is presented partly ,the much complex dynamic action was appeared ,it is very difficult that analysis of the hybrid systems function's security and state's reachability.
All tasks were worked for linear hybrid system formal verification. Linear system has the characteristic that its reachable set is convex hull if its initial region is convex hull. The subsystem is linear system in the hybrid system`s invariable set.The linear hybrid system verification process can be simplified.This thesis used crude oil heat process as example, it was modelled, the system was verified by the formal verification technique based on flow pipe and simplified flow pipe, the system's security and reachability was analyzed,this provided a reference for linear hybrid system verification.
The main work in this thesis is as follows:
1. The verification method based on flow pipe is analyzed, includes: the necessary of partition was analyzed, over approximate flow pipe, the relationship of over approximate flow pipe and quotient transition systems' establishment was analyzed.
2. The verification tools were compared. CheckMate was a verification tool based on flow pipe, its function models was introduced in detail.
3. The crude oil heater process run principle is analyzed,based on that the dynamical model is built,the verification problem is abstracted; hybrid automata model is established, the system`s state reachablity and function security is analyzed used the verification method based on flow pipe, verification result is worked out. The influence on the verification result used the different step in the verification process.
4. The crude oil heat process was verified by the verification method based on simplified flow pipe, The verification result was presented and analyzed. There is a compare between the verification results, they were presented by verification method based on flow pipe and simplified flow pipe. Their conservatism and computation costs were analyzed.
引文
[1]蒋慰孙,2000年化工自动化展望,化工自动化与仪表,1994,(01).
[2] A.Balluchi,M.D.Benedetto ,C.Pinello ,et,Cut-off in engine control:A hybrid system approach, In: Proceeding of the Conference on Decision and Control.1997,5:4720-4725.
[3] Krasovskii.N.N, The Theory of Control of Motion,Nauka,Moscow,1968.
[4] Lee.E.B,Markus.L,Foundation of Optional Control Theory,Wiley,New York,1961.
[5] W.Zhang,M.S.Branicky,S.M.Philips,Stability of Networked Control Systems,Control systems Magazine,IEEE,2001,21(1):84-99.
[6] C.Livadas,J.Analysis,N.Lynch,High-level Modeling And Analysis of The Traffic Alert and Collision Avoidance System,Proceedings of IEEE,2000,88(7):926-948.
[7]林海,混合系统稳定性及控制若干问题的研究,中国科学院自动化研究所,2000.
[8] H.S.Witsenhausen,A Class of Hybrid-State Continuous-Time Dynamical Systems.IEEE Transaction on Automatic Control,Vol,11,1987,pp.665-683.
[9] L.Tavenini,Differential Automata and Their Discrete Simulators,Nonlinear Analysis、Theory、Methods and Applications,Vol,11,1987,pp.665-683.
[10] M.S.Branicky,V.S.Borkar,S.K.Mitter,A Unified Framework for Hybrid Control、Model and Optional Control Theory,IEEE Trans, Automata,Control,Vol,43,No.1,pp.31-45,Jan 1998.
[11] M.S.Branicky,Studies in Hybrid Systems:Modeling Analysis and Control,Ph.D,Thesis,LIDS-Th2304,Laboratory for Information and Decision systems,MIT.
[12] Thomas A.Henzinger,The Theory of Hybrid Automata,The Proceedings of The 11th Annual Symposium on Logic in Computer Science,IEEE Computer Society Press,1996,pp278-292.
[13] Henzinger.T.A and S.Sastry,Hybrid Systems:Computation and Control,LNCS 1386,Springer,1998.
[14] A.Vander Shafe,H.Schamacher,An Introduction to Hybrid Dynamical Systems,Springer-Verlag,2000.
[15] Special Issue on Hybrid Petri Nets, A.D.Febbraro, Discrete Event Dynamical Systems: Theory and Applications,Vol.11,No.1/2,2001.
[16] H.Ye,A.N.Michel,L.Hou, Stability Theory for Hybrid Dynamical Systems,IEEE Transaction on Automatic Control ,Vol.43,No.4. 1998,pp.461-474.
[17] Branicky.M,Multiple Lyapunov Functions and Other Analysis Tool for Switched and Hybrid Systems,IEEE Transactions on Automatic Control, 1998,43:475-482.
[18] Horn.C,Ramadge.P.J,Robustness Issues for Hybrid System .In Proc of 34th CDC,New Orens,LA,1994,pp.1467-1472.
[19]张苗苗,混合系统的离散模型近似及形式验证.上海交通大学.2000.
[20] A.Chutinan, B.Krogh, Verification of Polyhedral Invariant Hybrid Automata Using Polygonal Flow Pipe Approxiamations .Hybrid Systems: Computation and Control.LNCS Vol.1569,Springer-Verlag,1999.pp.76-90.
[21] Ansgar Fehnker,and Bruce H.Krogh,Hybrid System Verification is Not a Sinecure.Proceedings of ht 2en Int.Symp. on Automated technology for Verification and Analysis.LNCS Vol.3299,Springer- Verlag,2004.pp.263-277.
[22] Claire J. Tomlin, Ian Mitchell, Alexandre M. Bayen, and Meeko Oishi, Computational Techniques for the Verification of Hybrid Systems. Proceedings of the IEEE, vol. 88, no. 7, 2000.
[23]A.M.Bayen,E.Cruck,and C. J.Tomlin,Guaranteed Over approximationsof Unsafe Sets for Continuous and Hybrid Systems: Solving the Hamilton-JacobiEquation Using Viability Techniques.Hybrid Systems:Computation and Control LNCS Vol.2289,Springer-Verlag,2002.pp.90-104.
[24] E. Asarin, T. Dang, O. Maler, dldt:A Verification Tool for Hybridsystems.Proceedings of the 40th IEEE Conference on Decision andControl. 2001.3 .pp.2893-2898.
[25]李辉.基于可达集过近似的混合系统验证方法[D].合肥工业大学, 2007.
[26] M.Broucke,M.D.Di Benedetto,S.Di Gennaro,and A Sangiovanni- Vincentelli, Optimal Control Using Bisimulations: Implementation Hybrid Systems:Computaion and Control.LNCS Vol.2034,Springer- Verlag,2001.pp.175-188.
[27]张学军,具有复杂连续动态混合系统的形式验证[D].上海交通大学. 2000.
[28] Laferriere G ,Pappas G J ,Sastry S .Hybrid systems with finitebisimulations[R].Technical Report UCB/ERL M98/15,University of California at Berkeley, April 1998.
[29] Chutinan A.Hybrid system verification using discrete model approximations.Ph. D thesis, CamegieMellon University,1999,5.
[30]边计年,薛宏熙,苏明,吴为民.数字系统设计自动化(第二版).2005.
[31] Clarke E M, Grumberg Jr O, Peled D A. Model Checking[M], Cambridge, Massachusetts: The MIT Press, 1999.
[32] Sistla AP, Clarke EM. The complexity of propositional linear temporal logics. Journal of the ACM, 1985,32(3):733~749.
[33] Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite state concurrent system using temporal logical specification. ACM Trans. on Programming Language and Systems, 1986,8(2):244~263.
[34]蒋屹新,林闯,曲扬,尹浩.基于petri网的模型检测研究.软件学报[J], Vol.15 , No.9 P.1265-1276.
[35] M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time. Acta Informatica 20(1983):207-226.
[36] E. M. Clarke, E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, LNCS 131. Springer, 1981.
[37] E. M. Clarke, E. A. Emerson. Characterizing correctness properties of parallel using fixpoints. In LNCS 85, Automata, Languages and Programming, pp.169-181. Springer, 1980.
[38] Chutinan A. Krogh Bruth, Verification of Infinite-State Dynamic Systems Using Approximate Quotient Transition systems. IEEE Transaction on Automatic Control 2001. 46:1401-1410.
[39]张雅顺.混合系统的形式验证方法及其应用[D].合肥工业大学硕士论文, 2006.5.
[40] Alur R, Courcoubetis C, Halbwachs N,etc. The algorithmic analysis of hybrid systems. Theoretical Computer Science 1995,138:3-34.
[41] R.Alur , Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, LNCS 736, Hybrid Systems, Springer-Verlag, 1993, pages 209-229.
[42] J. Lygeros, D .N. Godbole and S. Sastry, Multiagent Hybrid System Design Using Game Theory and Optimal Control, Proc. of the 35th CDC, Kobe, Japan, December, 1996, pages 1190 -1195.
[43] A. Nerode and W. Kohn, Multiple Agent Hybrid Control Architecture, Lecture Notes in Computer Science Vol.736, Hybrid Systems, Springer-Verlag, 1993, pages 297-316.
[44] S. N. Simic, K. Johansson, S. Sastry and J. Lygeros. Towards a geometric theory of hybrid systems, Jan. 2000.
[45] P. J. Antsaklis, J. A. Stiver and M. Lemmon, Hybrid System Modeling and Autonomous Control Systems, LNCS 736, Hybrid Systems, Springer-Verlag, 1993, pages 366-392.
[46] J. A. Stiver and P. J. Antsaklis, Modeling and Analysis of Hybrid Control Systems, Proc.of the 31st CDC, Tucson, Arizona, 1992, pages 3748-3751.
[47] E.K.Kornoushenko,“Finite-automation approximation to the behavior of continuous plants,”Automat. Rem. Control, vol. 36, no. 12, pp. 2068–2074, 1975.
[48] A. Puri, P. Varaiya, and V. Borkar,“ε-approximation of differential inclusions,”in Hybrid Systems III: Verification and Control, R. Alur, T. A. Henzinger, and E. D. Sontag, Eds. New York: Springer-Verlag, 1996, pp. 362–376.
[49] O. Stursberg, S. Kowalewski, and S. Engell,“On the generation of timed discrete approximations for continuous systems,”Math. Model. Syst. Special Issue Discrete-Event Models Contin. Syst, vol. 6, no. 1, pp. 51–70, 2000.
[50] T. A. Henzinger, P.-H. Ho, and H. Wong-Toi,“Algorithmic analysis of nonlinear hybrid systems,”IEEE Trans. Automat. Contr, vol. 43, pp. 540–554, Apr. 1998.
[51] Stursberg O and Krogh B H. Efficient Representation and Computation of Reachable Sets for Hybrid Systems. In Hybrid Systems: Computation and Control, Springer-Series: LNCS 2623, 2003, 482-497.
[52] Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Hybrid Systems: Computation and Control. Volume 1790 of LNCS., Springer (2000) 73–88.
[53] Kurzhanski, A., Varaiya, P.: Ellipsiodal techniques for reachability analysis. In: Hybrid Systems: Computation and Control. Vol.1790 of LNCS,Springer 2000:202–214.
[54] Larsen, Kim G., Paul Pettersson, and Wang Yi. Uppaal: Status andDevelopments[A]. Proceedings of International Conference on Computer Aided Verification[C]. LNCS 1254, Springer-Verlag, 1997. 456-459.
[55] C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The Tool Kronos[A]. Hybrid System III, Verification and Control[C]. LNCS 1066, Springer-Verlag, 1996. 208-219.
[56] Thomas A .Henzinger,Pei-Hsin Ho,and Howard Wong-Toi,Hytech:A Model Checker for Hybrid Systems. Software Tools for Technology Transfer. 1997(1):9p.110-122
[57]T.Henzinger, Pei-Hsin Ho, and Howard Wong-Toi, Beyond Hytech: Hybrid Systems Analysis Using Interval Numerical Methods. HybridSystems:Computational and Control.LNCSVol.1790,Springer,2000. 130-144
[58] E. Asarin, T. Dang, O. Maler. d/dt: A Verification Tool for Hybrid systems[A]. Proceedings of the 40th IEEE Conference on Decision and Control[C]. Orlando, Florida, USA, 2001. 2893-2898.
[59]B.Silva,K.Richieson,B.Krogh and A.Chutinan,Modeling and VerifyingHybrid Dynamic Systems Using CheckMate[A].Proceedings of the 4thInternational Conference on Automation of Mixed Processes[C]. Dortmund, Germany: Shaker Verlag, 2000. 323-328.
[60] O.Sturberg,S.Kowalewski, J.Preussig, and H.Treseler, Block-diagramBased Modeling and Analysis of Hybrid Processes under Discrete Control. Journal Europeen des Systems Automatises(JESA),1998 32 (9-10):pp.1097-1118.
[61] Frehse, G. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. See Morari and Thiele 2005.
[62] Thomas A .Henzinger,Pei-Hsin Ho,and Howard Wang-Toi, Hytech:the Next Generation. Proceedings of the 16th IEEE Real-time Systems Syrn. IEEE Computer Society Press,1995.pp .56-65.
[63] Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi, Algorithmic analysis of Nonlinear Hybrid Systems. IEEE Transaction on Automatic Control,1998.43 (4):pp .540-554.
[64]钱家麟等著,管式加热炉[M],北京,烃加工出版社,1987,8.
[65]石油化学工业部石油规划设计院组织编审,管式加热炉工艺计算,北京石油化工出版社,1979.
[66]周培德.计算几何-算法分析与设计.北京:清华大学出版社,1999,pp57-87.
[67]参考文献:华彤文、陈景祖,等.普通化学原理[M].第3版.北京大学出版社,2005年.
[2] A.Balluchi,M.D.Benedetto ,C.Pinello ,et,Cut-off in engine control:A hybrid system approach, In: Proceeding of the Conference on Decision and Control.1997,5:4720-4725.
[3] Krasovskii.N.N, The Theory of Control of Motion,Nauka,Moscow,1968.
[4] Lee.E.B,Markus.L,Foundation of Optional Control Theory,Wiley,New York,1961.
[5] W.Zhang,M.S.Branicky,S.M.Philips,Stability of Networked Control Systems,Control systems Magazine,IEEE,2001,21(1):84-99.
[6] C.Livadas,J.Analysis,N.Lynch,High-level Modeling And Analysis of The Traffic Alert and Collision Avoidance System,Proceedings of IEEE,2000,88(7):926-948.
[7]林海,混合系统稳定性及控制若干问题的研究,中国科学院自动化研究所,2000.
[8] H.S.Witsenhausen,A Class of Hybrid-State Continuous-Time Dynamical Systems.IEEE Transaction on Automatic Control,Vol,11,1987,pp.665-683.
[9] L.Tavenini,Differential Automata and Their Discrete Simulators,Nonlinear Analysis、Theory、Methods and Applications,Vol,11,1987,pp.665-683.
[10] M.S.Branicky,V.S.Borkar,S.K.Mitter,A Unified Framework for Hybrid Control、Model and Optional Control Theory,IEEE Trans, Automata,Control,Vol,43,No.1,pp.31-45,Jan 1998.
[11] M.S.Branicky,Studies in Hybrid Systems:Modeling Analysis and Control,Ph.D,Thesis,LIDS-Th2304,Laboratory for Information and Decision systems,MIT.
[12] Thomas A.Henzinger,The Theory of Hybrid Automata,The Proceedings of The 11th Annual Symposium on Logic in Computer Science,IEEE Computer Society Press,1996,pp278-292.
[13] Henzinger.T.A and S.Sastry,Hybrid Systems:Computation and Control,LNCS 1386,Springer,1998.
[14] A.Vander Shafe,H.Schamacher,An Introduction to Hybrid Dynamical Systems,Springer-Verlag,2000.
[15] Special Issue on Hybrid Petri Nets, A.D.Febbraro, Discrete Event Dynamical Systems: Theory and Applications,Vol.11,No.1/2,2001.
[16] H.Ye,A.N.Michel,L.Hou, Stability Theory for Hybrid Dynamical Systems,IEEE Transaction on Automatic Control ,Vol.43,No.4. 1998,pp.461-474.
[17] Branicky.M,Multiple Lyapunov Functions and Other Analysis Tool for Switched and Hybrid Systems,IEEE Transactions on Automatic Control, 1998,43:475-482.
[18] Horn.C,Ramadge.P.J,Robustness Issues for Hybrid System .In Proc of 34th CDC,New Orens,LA,1994,pp.1467-1472.
[19]张苗苗,混合系统的离散模型近似及形式验证.上海交通大学.2000.
[20] A.Chutinan, B.Krogh, Verification of Polyhedral Invariant Hybrid Automata Using Polygonal Flow Pipe Approxiamations .Hybrid Systems: Computation and Control.LNCS Vol.1569,Springer-Verlag,1999.pp.76-90.
[21] Ansgar Fehnker,and Bruce H.Krogh,Hybrid System Verification is Not a Sinecure.Proceedings of ht 2en Int.Symp. on Automated technology for Verification and Analysis.LNCS Vol.3299,Springer- Verlag,2004.pp.263-277.
[22] Claire J. Tomlin, Ian Mitchell, Alexandre M. Bayen, and Meeko Oishi, Computational Techniques for the Verification of Hybrid Systems. Proceedings of the IEEE, vol. 88, no. 7, 2000.
[23]A.M.Bayen,E.Cruck,and C. J.Tomlin,Guaranteed Over approximationsof Unsafe Sets for Continuous and Hybrid Systems: Solving the Hamilton-JacobiEquation Using Viability Techniques.Hybrid Systems:Computation and Control LNCS Vol.2289,Springer-Verlag,2002.pp.90-104.
[24] E. Asarin, T. Dang, O. Maler, dldt:A Verification Tool for Hybridsystems.Proceedings of the 40th IEEE Conference on Decision andControl. 2001.3 .pp.2893-2898.
[25]李辉.基于可达集过近似的混合系统验证方法[D].合肥工业大学, 2007.
[26] M.Broucke,M.D.Di Benedetto,S.Di Gennaro,and A Sangiovanni- Vincentelli, Optimal Control Using Bisimulations: Implementation Hybrid Systems:Computaion and Control.LNCS Vol.2034,Springer- Verlag,2001.pp.175-188.
[27]张学军,具有复杂连续动态混合系统的形式验证[D].上海交通大学. 2000.
[28] Laferriere G ,Pappas G J ,Sastry S .Hybrid systems with finitebisimulations[R].Technical Report UCB/ERL M98/15,University of California at Berkeley, April 1998.
[29] Chutinan A.Hybrid system verification using discrete model approximations.Ph. D thesis, CamegieMellon University,1999,5.
[30]边计年,薛宏熙,苏明,吴为民.数字系统设计自动化(第二版).2005.
[31] Clarke E M, Grumberg Jr O, Peled D A. Model Checking[M], Cambridge, Massachusetts: The MIT Press, 1999.
[32] Sistla AP, Clarke EM. The complexity of propositional linear temporal logics. Journal of the ACM, 1985,32(3):733~749.
[33] Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite state concurrent system using temporal logical specification. ACM Trans. on Programming Language and Systems, 1986,8(2):244~263.
[34]蒋屹新,林闯,曲扬,尹浩.基于petri网的模型检测研究.软件学报[J], Vol.15 , No.9 P.1265-1276.
[35] M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time. Acta Informatica 20(1983):207-226.
[36] E. M. Clarke, E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, LNCS 131. Springer, 1981.
[37] E. M. Clarke, E. A. Emerson. Characterizing correctness properties of parallel using fixpoints. In LNCS 85, Automata, Languages and Programming, pp.169-181. Springer, 1980.
[38] Chutinan A. Krogh Bruth, Verification of Infinite-State Dynamic Systems Using Approximate Quotient Transition systems. IEEE Transaction on Automatic Control 2001. 46:1401-1410.
[39]张雅顺.混合系统的形式验证方法及其应用[D].合肥工业大学硕士论文, 2006.5.
[40] Alur R, Courcoubetis C, Halbwachs N,etc. The algorithmic analysis of hybrid systems. Theoretical Computer Science 1995,138:3-34.
[41] R.Alur , Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, LNCS 736, Hybrid Systems, Springer-Verlag, 1993, pages 209-229.
[42] J. Lygeros, D .N. Godbole and S. Sastry, Multiagent Hybrid System Design Using Game Theory and Optimal Control, Proc. of the 35th CDC, Kobe, Japan, December, 1996, pages 1190 -1195.
[43] A. Nerode and W. Kohn, Multiple Agent Hybrid Control Architecture, Lecture Notes in Computer Science Vol.736, Hybrid Systems, Springer-Verlag, 1993, pages 297-316.
[44] S. N. Simic, K. Johansson, S. Sastry and J. Lygeros. Towards a geometric theory of hybrid systems, Jan. 2000.
[45] P. J. Antsaklis, J. A. Stiver and M. Lemmon, Hybrid System Modeling and Autonomous Control Systems, LNCS 736, Hybrid Systems, Springer-Verlag, 1993, pages 366-392.
[46] J. A. Stiver and P. J. Antsaklis, Modeling and Analysis of Hybrid Control Systems, Proc.of the 31st CDC, Tucson, Arizona, 1992, pages 3748-3751.
[47] E.K.Kornoushenko,“Finite-automation approximation to the behavior of continuous plants,”Automat. Rem. Control, vol. 36, no. 12, pp. 2068–2074, 1975.
[48] A. Puri, P. Varaiya, and V. Borkar,“ε-approximation of differential inclusions,”in Hybrid Systems III: Verification and Control, R. Alur, T. A. Henzinger, and E. D. Sontag, Eds. New York: Springer-Verlag, 1996, pp. 362–376.
[49] O. Stursberg, S. Kowalewski, and S. Engell,“On the generation of timed discrete approximations for continuous systems,”Math. Model. Syst. Special Issue Discrete-Event Models Contin. Syst, vol. 6, no. 1, pp. 51–70, 2000.
[50] T. A. Henzinger, P.-H. Ho, and H. Wong-Toi,“Algorithmic analysis of nonlinear hybrid systems,”IEEE Trans. Automat. Contr, vol. 43, pp. 540–554, Apr. 1998.
[51] Stursberg O and Krogh B H. Efficient Representation and Computation of Reachable Sets for Hybrid Systems. In Hybrid Systems: Computation and Control, Springer-Series: LNCS 2623, 2003, 482-497.
[52] Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Hybrid Systems: Computation and Control. Volume 1790 of LNCS., Springer (2000) 73–88.
[53] Kurzhanski, A., Varaiya, P.: Ellipsiodal techniques for reachability analysis. In: Hybrid Systems: Computation and Control. Vol.1790 of LNCS,Springer 2000:202–214.
[54] Larsen, Kim G., Paul Pettersson, and Wang Yi. Uppaal: Status andDevelopments[A]. Proceedings of International Conference on Computer Aided Verification[C]. LNCS 1254, Springer-Verlag, 1997. 456-459.
[55] C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The Tool Kronos[A]. Hybrid System III, Verification and Control[C]. LNCS 1066, Springer-Verlag, 1996. 208-219.
[56] Thomas A .Henzinger,Pei-Hsin Ho,and Howard Wong-Toi,Hytech:A Model Checker for Hybrid Systems. Software Tools for Technology Transfer. 1997(1):9p.110-122
[57]T.Henzinger, Pei-Hsin Ho, and Howard Wong-Toi, Beyond Hytech: Hybrid Systems Analysis Using Interval Numerical Methods. HybridSystems:Computational and Control.LNCSVol.1790,Springer,2000. 130-144
[58] E. Asarin, T. Dang, O. Maler. d/dt: A Verification Tool for Hybrid systems[A]. Proceedings of the 40th IEEE Conference on Decision and Control[C]. Orlando, Florida, USA, 2001. 2893-2898.
[59]B.Silva,K.Richieson,B.Krogh and A.Chutinan,Modeling and VerifyingHybrid Dynamic Systems Using CheckMate[A].Proceedings of the 4thInternational Conference on Automation of Mixed Processes[C]. Dortmund, Germany: Shaker Verlag, 2000. 323-328.
[60] O.Sturberg,S.Kowalewski, J.Preussig, and H.Treseler, Block-diagramBased Modeling and Analysis of Hybrid Processes under Discrete Control. Journal Europeen des Systems Automatises(JESA),1998 32 (9-10):pp.1097-1118.
[61] Frehse, G. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. See Morari and Thiele 2005.
[62] Thomas A .Henzinger,Pei-Hsin Ho,and Howard Wang-Toi, Hytech:the Next Generation. Proceedings of the 16th IEEE Real-time Systems Syrn. IEEE Computer Society Press,1995.pp .56-65.
[63] Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi, Algorithmic analysis of Nonlinear Hybrid Systems. IEEE Transaction on Automatic Control,1998.43 (4):pp .540-554.
[64]钱家麟等著,管式加热炉[M],北京,烃加工出版社,1987,8.
[65]石油化学工业部石油规划设计院组织编审,管式加热炉工艺计算,北京石油化工出版社,1979.
[66]周培德.计算几何-算法分析与设计.北京:清华大学出版社,1999,pp57-87.
[67]参考文献:华彤文、陈景祖,等.普通化学原理[M].第3版.北京大学出版社,2005年.