基于层次模型的混合系统形式化分析与验证
|
摘要
随着科技的进步,尤其是电子技术的长足发展,以及社会生产和生活的需求,计算机相关的技术对各种技术领域的涉及程度越来越广泛和深入,这就导致了以连续与离散行为共存为特点的混合系统的广泛使用。我们从形式化地角度来研究混合系统。目前混合系统的形式化分析、验证与模拟方法主要有两类,即演算推演法和混合自动机法,二者的理论都已经比较成熟,都要求将实例空间映射到理论空间,而后应用这些成熟的理论和方法进行分析验证。但是上述两个空间的映射,即建模方法,目前还比较混乱,并没有形成统一的有效框架,还处于具体实例具体分析的手工阶段。
混合系统的研究对象包含控制系统、嵌入式系统和Cyber Physical系统等,这些系统的设计阶段都大量采用了成熟的层次化设计思路,并生成大量的层次化设计文档。那么快速准确地从层次化设计中得到混合系统形式化分析模型,并对此模型进行分析验证的工作就非常具有实际意义。
本文研究将这种工业界常用的层次化设计,直接对应到混合系统形式化分析对象的方法。我们的依据是一种广泛采用的层次化设计概念模型[24],首先研究这种层次化概念模型的符号化表示,即层次化形式模型,而后基于此形式模型,探讨时段演算推演方法及混合自动机方法的语义,将此层次化混合系统形式模型映射为时段公式或混合自动机,最后按照(扩展)时段演算和混合自动机理论进行分析验证,并给出实例来阐述这种方法的可行性。
The evolution of electronics, as well as the requirements of human activities, makes computer related technologies involving in each field of engineering, widely and deeply, e.g., the reason of why the hybrid systems, characterized by both discrete and continuous behaviors, are common now. We study the hybrid system in a formal way. The formal methods of hybrid system contain formal analysis, formal verification and validation, all of which are based on calculus and hybrid automata generally. The theories of these calculus or automata are well-studied and extended, but modeling is now a challenge.
Control system, embedded system and cyber physical system belong to hy-brid systems, each of them adopts hierarchical methodology while designing. Then it is basic and significant to quickly generate the accurate formal model from these hierarchical designs.
In this thesis, we try to find a direct theoretical way that maps the hierar-chical designs into the formal model of hybrid system, e.g., with a widely used hierarchical design model[24], we symbolize the hierarchical design and get the hierarchial formal model. Then we study the semantics of both duration calculus and hybrid automata based on the hierarchical formal model, and then study the way of analysis and validation with some practical case studies.
混合系统的研究对象包含控制系统、嵌入式系统和Cyber Physical系统等,这些系统的设计阶段都大量采用了成熟的层次化设计思路,并生成大量的层次化设计文档。那么快速准确地从层次化设计中得到混合系统形式化分析模型,并对此模型进行分析验证的工作就非常具有实际意义。
本文研究将这种工业界常用的层次化设计,直接对应到混合系统形式化分析对象的方法。我们的依据是一种广泛采用的层次化设计概念模型[24],首先研究这种层次化概念模型的符号化表示,即层次化形式模型,而后基于此形式模型,探讨时段演算推演方法及混合自动机方法的语义,将此层次化混合系统形式模型映射为时段公式或混合自动机,最后按照(扩展)时段演算和混合自动机理论进行分析验证,并给出实例来阐述这种方法的可行性。
The evolution of electronics, as well as the requirements of human activities, makes computer related technologies involving in each field of engineering, widely and deeply, e.g., the reason of why the hybrid systems, characterized by both discrete and continuous behaviors, are common now. We study the hybrid system in a formal way. The formal methods of hybrid system contain formal analysis, formal verification and validation, all of which are based on calculus and hybrid automata generally. The theories of these calculus or automata are well-studied and extended, but modeling is now a challenge.
Control system, embedded system and cyber physical system belong to hy-brid systems, each of them adopts hierarchical methodology while designing. Then it is basic and significant to quickly generate the accurate formal model from these hierarchical designs.
In this thesis, we try to find a direct theoretical way that maps the hierar-chical designs into the formal model of hybrid system, e.g., with a widely used hierarchical design model[24], we symbolize the hierarchical design and get the hierarchial formal model. Then we study the semantics of both duration calculus and hybrid automata based on the hierarchical formal model, and then study the way of analysis and validation with some practical case studies.
引文
[1]李晓山,周巢尘.时段演算综述.计算机学报,17(11)：842-851,1994.
[2]韩俊刚,杜慧敏.数字硬件的形式化验证.2001.
[3]Cyber-physical systems. Program Announcements & Information. The Na-tional Science Foundation of USA.,2008.
[4]杜承烈.机物系统研究现状.2010.
[5]R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. THEORETICAL COMPUTER SCIENCE,138:3-34,1995.
[6]J. M. B. Braman and R. M. Murray. Probabilistic safety analysis of sensor-driven hybrid automata. In Hybrid Systems:Computation and Control, 2009.
[7]Alberto Casagrande, Kevin Casey, Rachele Falchi, Carla Piazza, Benedetto Ruperti, Giannina Vizzotto, and Bud Mishra. Translating time-course gene expression profiles into semi-algebraic hybrid automata via dimensionality reduction. In Proceedings of the 2nd international conference on Algebraic biology, AB'07, pages 51-65, Berlin, Heidelberg,2007. Springer-Verlag.
[8]Alberto Casagrande, Pietro Corvaja, Carla Piazza, and Bud Mishra. Decid-able compositions of o-minimal automata.
[9]Christos Cassandras and Stephane Lafortune. Introduction to Discrete Event Systems. Hardcover, ISBN 978-0-387-33332-8.
[10]Zhou Chaochen, C. A. R. Hoare, and Anders P. Ravn. A calculus of dura-tions. Information Processing Letters,40(5):269-276, December 1991.
[11]H. Dierks. Synthesizing controllers from real-time specifications. IEEE Trans. CAD,18(1):33-43,1999.
[12]Abbas Edalat and Dirk Pattinson. Denotational semantics of hybrid au-tomata. In Proc. FoSSaCS 2006, pages 231-245,2006.
[13]C. Seatzu F. Balduzzi, A. Giua. Modelling automated manufacturing systems with hybrid automata. Proc. Work, on Formal Methods and Manufacturing (Zaragoza, Spain),138:33-48,1999.
[14]Georg Frey and Lothar Litz. Formal methods in PLC programming. IEEE International Conference on Systems, Man, and Cybernetics, pages 2431-2436,2000.
[15]Anping He,, Xiaoyu Song, William N. N. Hung, Ming Gu, Jinzhao Wu, and Lian Li. Validating programmable logic controllers with duration cal-culus (unpublished), (submitted to) Transactions on Systems, Man, and Cybernetics-Part A:Systems and Humans.
[16]Anping He, William N.N. Hung, Jinzhao Wu, and Lian Li. Mathemati-cal analysis of stage-based programmable logic controller. Computers and Mathematics with Applications,61:1769-1785,2011.
[17]Anping He, Xiaoyu Song, William N.N Hung, Ming Gu, Jinzhao Wu, and Lian Li. A case study of stage suspended boom systems with hybrid au-tomata (unpublished).(submitted to) IEEE Transactions on Automation Science and Engineering.
[18]Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-toi. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Con-trol.43:225-238.1996.
[19]Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What's decidable about hybrid automata? In Journal of Computer and System Sciences, pages 373-382. ACM Press,1995.
[20]L.E. Holloway and B.H. Krogh. Synthesis of feedback control logic for a class of controlled Petri nets. IEEE Trans. Automatic Control,35(5):514-523,1989.
[21]Padmanabhan Krishnan. Hybrid event structures,1996.
[22]Bud Mishra. Algebraic systems biology:theses and hypotheses. In Proceed-ings of the 2nd international conference on Algebraic biology, AB'07, pages 1-14, Berlin, Heidelberg,2007. Springer-Verlag.
[23]Olaf Muller and Thomas Stauner. Modelling and verification using linear hybrid automata-a case study,1996.
[24]Magnus Morin and Simin Nadjm-tehrani. Real-time hierarchical control. IEEE Software,9(5):51-57, Sep./Oct.1992.
[25]Tadao Murata. Petri nets:Properties, analysis and applications. Proceedings of the IEEE, vol.77, no.4,,1989.
[26]Simin Nadjm-Tehrani and Jan-Erik Stromberg. JAS-95 Lite:Modelling and Formal Analysis of Dynamic Properties. Technical Report LITH-IDA-R-96-41, Dept. of Computer and Information Science, Linkoping University, December 1996.
[27]Simin Nadjm-Tehrani and Jan-Erik Stromberg. Formal verification of dy-namic properties in an aerospace application. Formal Methods in System Design,14(2):135-169, March 1999.
[28]P. Peleties and R. DeCarlo. A modeling strategy for hybrid systems based on event structures. Discr. Event Dyn. Syst.. Theory Appl,1993.
[29]Andreas Podelski and Silke Wagner. Model checking of hybrid systems: From reachability towards stability. In Hybrid Systems:Computation and Control, volume 3927 of LNCS. Springer,2006.
[30]K. Schneider R. Gentilini and B. Mishra. Successive abstractions of hybrid automata for monotonic ctl model checking. LFCS Proceedings of the inter-national symposium on Logical Foundations of Computer Science,2007.
[31]A. P. Ravn. Design of embedded real-time computing systems. Technical Report IDTR: 1995-170, Dept. of Computer Science, Technical University of Denmark, October 1995.
[32]Klein. S, Frey. G, and Minas. M. Plc programming with signal interpreted petri nets. Proceedings of the International Conference on Application and Theory of Petri Nets (ICATPN 2003),2003.
[33]Klein. S, Frey. G, and Minas. M. Verification and implementation of de-pendable controllers. Third International Conference on Dependability of Computer System DepCoS-RELCOMEX,2008.
[34]SIEMENS. S7-200 Programmable Controller System Manual.
[35]Richard Susta. Verification of PLC Programs. PhD thesis, CTU-FEE Prague,2003. Revised edition.
[36]Kok Kiong Tan, Qing-Guo Wang, and Chang Chieh Hang. Advances in PID Control. Springer-Verlag,1999.
[37]J. G. Thistle and W. M. Wonham. Control problems in a temporal logic framework. International Joumal of Control,44(4):943-976,1986.
[38]Tim Wescott. PID Without a PhD. Embedded Systems Programming, Oc-tober 2000.
[39]Brian C. Williams, Melvin Michael Henry, and Melvin Michael Henry. Model-based estimation of probabilistic hybrid automata.2002.
[2]韩俊刚,杜慧敏.数字硬件的形式化验证.2001.
[3]Cyber-physical systems. Program Announcements & Information. The Na-tional Science Foundation of USA.,2008.
[4]杜承烈.机物系统研究现状.2010.
[5]R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. THEORETICAL COMPUTER SCIENCE,138:3-34,1995.
[6]J. M. B. Braman and R. M. Murray. Probabilistic safety analysis of sensor-driven hybrid automata. In Hybrid Systems:Computation and Control, 2009.
[7]Alberto Casagrande, Kevin Casey, Rachele Falchi, Carla Piazza, Benedetto Ruperti, Giannina Vizzotto, and Bud Mishra. Translating time-course gene expression profiles into semi-algebraic hybrid automata via dimensionality reduction. In Proceedings of the 2nd international conference on Algebraic biology, AB'07, pages 51-65, Berlin, Heidelberg,2007. Springer-Verlag.
[8]Alberto Casagrande, Pietro Corvaja, Carla Piazza, and Bud Mishra. Decid-able compositions of o-minimal automata.
[9]Christos Cassandras and Stephane Lafortune. Introduction to Discrete Event Systems. Hardcover, ISBN 978-0-387-33332-8.
[10]Zhou Chaochen, C. A. R. Hoare, and Anders P. Ravn. A calculus of dura-tions. Information Processing Letters,40(5):269-276, December 1991.
[11]H. Dierks. Synthesizing controllers from real-time specifications. IEEE Trans. CAD,18(1):33-43,1999.
[12]Abbas Edalat and Dirk Pattinson. Denotational semantics of hybrid au-tomata. In Proc. FoSSaCS 2006, pages 231-245,2006.
[13]C. Seatzu F. Balduzzi, A. Giua. Modelling automated manufacturing systems with hybrid automata. Proc. Work, on Formal Methods and Manufacturing (Zaragoza, Spain),138:33-48,1999.
[14]Georg Frey and Lothar Litz. Formal methods in PLC programming. IEEE International Conference on Systems, Man, and Cybernetics, pages 2431-2436,2000.
[15]Anping He,, Xiaoyu Song, William N. N. Hung, Ming Gu, Jinzhao Wu, and Lian Li. Validating programmable logic controllers with duration cal-culus (unpublished), (submitted to) Transactions on Systems, Man, and Cybernetics-Part A:Systems and Humans.
[16]Anping He, William N.N. Hung, Jinzhao Wu, and Lian Li. Mathemati-cal analysis of stage-based programmable logic controller. Computers and Mathematics with Applications,61:1769-1785,2011.
[17]Anping He, Xiaoyu Song, William N.N Hung, Ming Gu, Jinzhao Wu, and Lian Li. A case study of stage suspended boom systems with hybrid au-tomata (unpublished).(submitted to) IEEE Transactions on Automation Science and Engineering.
[18]Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-toi. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Con-trol.43:225-238.1996.
[19]Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What's decidable about hybrid automata? In Journal of Computer and System Sciences, pages 373-382. ACM Press,1995.
[20]L.E. Holloway and B.H. Krogh. Synthesis of feedback control logic for a class of controlled Petri nets. IEEE Trans. Automatic Control,35(5):514-523,1989.
[21]Padmanabhan Krishnan. Hybrid event structures,1996.
[22]Bud Mishra. Algebraic systems biology:theses and hypotheses. In Proceed-ings of the 2nd international conference on Algebraic biology, AB'07, pages 1-14, Berlin, Heidelberg,2007. Springer-Verlag.
[23]Olaf Muller and Thomas Stauner. Modelling and verification using linear hybrid automata-a case study,1996.
[24]Magnus Morin and Simin Nadjm-tehrani. Real-time hierarchical control. IEEE Software,9(5):51-57, Sep./Oct.1992.
[25]Tadao Murata. Petri nets:Properties, analysis and applications. Proceedings of the IEEE, vol.77, no.4,,1989.
[26]Simin Nadjm-Tehrani and Jan-Erik Stromberg. JAS-95 Lite:Modelling and Formal Analysis of Dynamic Properties. Technical Report LITH-IDA-R-96-41, Dept. of Computer and Information Science, Linkoping University, December 1996.
[27]Simin Nadjm-Tehrani and Jan-Erik Stromberg. Formal verification of dy-namic properties in an aerospace application. Formal Methods in System Design,14(2):135-169, March 1999.
[28]P. Peleties and R. DeCarlo. A modeling strategy for hybrid systems based on event structures. Discr. Event Dyn. Syst.. Theory Appl,1993.
[29]Andreas Podelski and Silke Wagner. Model checking of hybrid systems: From reachability towards stability. In Hybrid Systems:Computation and Control, volume 3927 of LNCS. Springer,2006.
[30]K. Schneider R. Gentilini and B. Mishra. Successive abstractions of hybrid automata for monotonic ctl model checking. LFCS Proceedings of the inter-national symposium on Logical Foundations of Computer Science,2007.
[31]A. P. Ravn. Design of embedded real-time computing systems. Technical Report IDTR: 1995-170, Dept. of Computer Science, Technical University of Denmark, October 1995.
[32]Klein. S, Frey. G, and Minas. M. Plc programming with signal interpreted petri nets. Proceedings of the International Conference on Application and Theory of Petri Nets (ICATPN 2003),2003.
[33]Klein. S, Frey. G, and Minas. M. Verification and implementation of de-pendable controllers. Third International Conference on Dependability of Computer System DepCoS-RELCOMEX,2008.
[34]SIEMENS. S7-200 Programmable Controller System Manual.
[35]Richard Susta. Verification of PLC Programs. PhD thesis, CTU-FEE Prague,2003. Revised edition.
[36]Kok Kiong Tan, Qing-Guo Wang, and Chang Chieh Hang. Advances in PID Control. Springer-Verlag,1999.
[37]J. G. Thistle and W. M. Wonham. Control problems in a temporal logic framework. International Joumal of Control,44(4):943-976,1986.
[38]Tim Wescott. PID Without a PhD. Embedded Systems Programming, Oc-tober 2000.
[39]Brian C. Williams, Melvin Michael Henry, and Melvin Michael Henry. Model-based estimation of probabilistic hybrid automata.2002.