基于Event-B的混合系统形式化：理论与实践
|
摘要
当今社会,混合系统在嵌入式系统开发中起着至关重要的作用。混合系统中,软件控制器控制外部环境的变化,以离散的方式由传感器规律地触发来检测环境状态,控制环境。相邻的控制器行为之间,环境以连续的方式变化。如何设计出与物理环境正确匹配的控制器已成为一大挑战。
众多学科都不断贡献于该领域,包括计算机、系统控制、模拟仿真等学科。在这些学科中,我们主要从事计算机学科的研究,但也与系统控制、模拟仿真等学科紧密相连。
计算机学科对混合系统的研究主要为系统验证,相比于其它研究,我们的研究不仅仅着重于系统验证,也同时着重于建模、证明、仿真。
我们的研究目如何构建正确的混合系统。确切地说,基于Event-B方法,我们研究自顶向下的混合系统开发方法：从需求文档,得到精化策略,而后建立系列的形式化模型,最终开发实现。模型开发基于系列的精化模型,使得系统能够以渐进的方式实现开发。在离散连续混合系统开发中,我们主要关注以下问题：定义良好的需求文档与精化策略、建立混合系统模型、实现模型精化、证明模型及精化的正确性、证明系统安全性质、实现系统仿真等。本文所展开的工作均围绕上述问题。本论文的主要贡献如下：
(i)方法学贡献基于Event-B方法,在形式化建模之前,首先要定义需求文档及精化策略。精化策略用于定义精化模型中对需求的考虑顺序,实现从形式化模型到需求文档的可追踪性,并用于检查形式化模型是否已完整考虑需求。本文提出制定需求文档与精化策略所应遵循的规则。
(ii)理论贡献提出Event-B含时间函数的混合系统的建模方法,并提出离散模型至连续模型的精化方法,以及该混合模型的分析验证方法。为支持复杂物理系统,我们扩展混合系统建模方法,引入一个新的方法,称为"Click",并基于该方法为混合系统的时间特性提出系统化的设计模式。对连续行为由微分方程定义的混合系统,在不解微分方程的前提下,我们研究微分方程性质的定理证明方法。该研究基于欧拉近似方法和非标准分析。
(iii)实践贡献该研究包含众多案例,用于分析所提出的理论及方法。案例涵盖核反应冷却控制、列车控制、飞机防碰撞系统、水箱控制等。这些案例不仅用于分析所提出的理论,也在一定程度上证明了理论的应用性。提出混合系统形式化开发的互补方法,包括模型仿真、传感器和执行器设计模式、隐式不变式发现方法等。
(iv)软件贡献为了互补Event-B形式化开发方法,将Event-B模型转化至Simulink模型,我们为Event-B言语的相应工具Rodin平台开发了插件,可以自动实现模型转化。
Nowadays, hybrid systems are very important in the development of embedded systems. In such systems, a piece of software, the controller, is supposed to manage an external situation, the environment. The controller works in a discrete fashion in that it is triggered regularly by detecting the status of the environment (using some sensors), and then reacts by sending some information to the environment (using some actuators). Between two successive controller detections and actions, the environment is evolving in a continuous way. The design of a controller that correctly matches the physical environment has become a challenge.
Various scientific community have contributed with their own approaches to this area:computer science, control, and modeling and simulation communities. We mainly place ourselves in the computer science community, but we also have some connections with the control community, and the modeling and simulation community.
Other works in computer science community mainly focus on software verifica-tion, here we would like to propose an approach that certainly focus on verification, but also on modeling, simulation, and proof. Our purpose is to construct hybrid systems in a correct fashion. More precisely, based on Event-B, we propose a top-down approach that supports the development of hybrid systems from requirements down to final development. For this, our con-struction is based on successive refinements, allowing the development to be done in a gradual fashion. In the development of hybrid system, we concentrate on the following key issues:well-defined requirement document and refinement strategy, modeling, refinement, proving, and simulation.
Here are the main contributions of this thesis:
(i) Methodology Contribution Based on Event-B, requirement document and refinement strategy need to be first defined before formal modelling. We insist a lot on the importance of writing a well defined requirement document and a careful refinement strategy. Before modeling, the refinement strategy is used to define clearly how the requirements can be gradually taken into account in successive refinements. It also helps us to trace the formal development back to the requirement document, and check whether we have taken all requirements into account. To achieve this, we propose some rules for defining the requirement document and the refinement strategy,
(ii) Theoretic Contribution We explain how hybrid systems with time function can be developed in Event-B and we show how we can transform a discrete approach to a continuous one. This is based on the usage of refinement. In order to support complex physical system, we extend the approach of model-ing hybrid systems with a new one called "Click":this constitutes a systematic design pattern for the time feature of hybrid systems. For those hybrid systems where the continuous parts are defined by differential equations, we try to give a theoretical approach on how to prove properties of differential equations without solving them. This work is based on solid mathematic foundations:the usage of Euler approximations and that of non standard analysis,
(iii) Practical Contribution This study contains many practical examples whose role is to explain our approach. Such examples cover nuclear cooling control, train control, aircraft collision avoidance, water tank, etc. We believe that examples are important to show that this approach to hybrid systems can be made practical. In order to improve the confidence in formal modeling, we also propose some complementary approaches for hybrid system development. This includes the usage Simulink and animation, the introduction of sensor and actuator pat-terns, and an implicit invariant discovery approach as well.
(iv) Software Contribution In order to complement formal development and translate Event-B model to Simulink model, we developed a plug-in for the Rodin platform. This plug-in can perform this translation automatically.
众多学科都不断贡献于该领域,包括计算机、系统控制、模拟仿真等学科。在这些学科中,我们主要从事计算机学科的研究,但也与系统控制、模拟仿真等学科紧密相连。
计算机学科对混合系统的研究主要为系统验证,相比于其它研究,我们的研究不仅仅着重于系统验证,也同时着重于建模、证明、仿真。
我们的研究目如何构建正确的混合系统。确切地说,基于Event-B方法,我们研究自顶向下的混合系统开发方法：从需求文档,得到精化策略,而后建立系列的形式化模型,最终开发实现。模型开发基于系列的精化模型,使得系统能够以渐进的方式实现开发。在离散连续混合系统开发中,我们主要关注以下问题：定义良好的需求文档与精化策略、建立混合系统模型、实现模型精化、证明模型及精化的正确性、证明系统安全性质、实现系统仿真等。本文所展开的工作均围绕上述问题。本论文的主要贡献如下：
(i)方法学贡献基于Event-B方法,在形式化建模之前,首先要定义需求文档及精化策略。精化策略用于定义精化模型中对需求的考虑顺序,实现从形式化模型到需求文档的可追踪性,并用于检查形式化模型是否已完整考虑需求。本文提出制定需求文档与精化策略所应遵循的规则。
(ii)理论贡献提出Event-B含时间函数的混合系统的建模方法,并提出离散模型至连续模型的精化方法,以及该混合模型的分析验证方法。为支持复杂物理系统,我们扩展混合系统建模方法,引入一个新的方法,称为"Click",并基于该方法为混合系统的时间特性提出系统化的设计模式。对连续行为由微分方程定义的混合系统,在不解微分方程的前提下,我们研究微分方程性质的定理证明方法。该研究基于欧拉近似方法和非标准分析。
(iii)实践贡献该研究包含众多案例,用于分析所提出的理论及方法。案例涵盖核反应冷却控制、列车控制、飞机防碰撞系统、水箱控制等。这些案例不仅用于分析所提出的理论,也在一定程度上证明了理论的应用性。提出混合系统形式化开发的互补方法,包括模型仿真、传感器和执行器设计模式、隐式不变式发现方法等。
(iv)软件贡献为了互补Event-B形式化开发方法,将Event-B模型转化至Simulink模型,我们为Event-B言语的相应工具Rodin平台开发了插件,可以自动实现模型转化。
Nowadays, hybrid systems are very important in the development of embedded systems. In such systems, a piece of software, the controller, is supposed to manage an external situation, the environment. The controller works in a discrete fashion in that it is triggered regularly by detecting the status of the environment (using some sensors), and then reacts by sending some information to the environment (using some actuators). Between two successive controller detections and actions, the environment is evolving in a continuous way. The design of a controller that correctly matches the physical environment has become a challenge.
Various scientific community have contributed with their own approaches to this area:computer science, control, and modeling and simulation communities. We mainly place ourselves in the computer science community, but we also have some connections with the control community, and the modeling and simulation community.
Other works in computer science community mainly focus on software verifica-tion, here we would like to propose an approach that certainly focus on verification, but also on modeling, simulation, and proof. Our purpose is to construct hybrid systems in a correct fashion. More precisely, based on Event-B, we propose a top-down approach that supports the development of hybrid systems from requirements down to final development. For this, our con-struction is based on successive refinements, allowing the development to be done in a gradual fashion. In the development of hybrid system, we concentrate on the following key issues:well-defined requirement document and refinement strategy, modeling, refinement, proving, and simulation.
Here are the main contributions of this thesis:
(i) Methodology Contribution Based on Event-B, requirement document and refinement strategy need to be first defined before formal modelling. We insist a lot on the importance of writing a well defined requirement document and a careful refinement strategy. Before modeling, the refinement strategy is used to define clearly how the requirements can be gradually taken into account in successive refinements. It also helps us to trace the formal development back to the requirement document, and check whether we have taken all requirements into account. To achieve this, we propose some rules for defining the requirement document and the refinement strategy,
(ii) Theoretic Contribution We explain how hybrid systems with time function can be developed in Event-B and we show how we can transform a discrete approach to a continuous one. This is based on the usage of refinement. In order to support complex physical system, we extend the approach of model-ing hybrid systems with a new one called "Click":this constitutes a systematic design pattern for the time feature of hybrid systems. For those hybrid systems where the continuous parts are defined by differential equations, we try to give a theoretical approach on how to prove properties of differential equations without solving them. This work is based on solid mathematic foundations:the usage of Euler approximations and that of non standard analysis,
(iii) Practical Contribution This study contains many practical examples whose role is to explain our approach. Such examples cover nuclear cooling control, train control, aircraft collision avoidance, water tank, etc. We believe that examples are important to show that this approach to hybrid systems can be made practical. In order to improve the confidence in formal modeling, we also propose some complementary approaches for hybrid system development. This includes the usage Simulink and animation, the introduction of sensor and actuator pat-terns, and an implicit invariant discovery approach as well.
(iv) Software Contribution In order to complement formal development and translate Event-B model to Simulink model, we developed a plug-in for the Rodin platform. This plug-in can perform this translation automatically.
引文
[1]J.-R. Abrial. Data semantics. In IFIP Working Conference Data Base Man-agement, pages 1-60,1974.
[2]J.-R. Abrial. The B-book:assigning programs to meanings. Cambridge Uni-versity Press, New York, NY, USA,1996.
[3]J.-R. Abrial. Refinement, decomposition and instantiation of discrete models. In Abstract State Machines, pages 17-40,2005.
[4]J.-R. Abrial. Faultless systems:Yes we can! IEEE Computer,42(9):30-36, 2009.
[5]J.-R. Abrial. Modeling in Event-B:System and Software Engineering. Cam-bridge University Press, New York, NY, USA,1st edition,2010.
[6]J.-R. Abrial. From Z to B and then Event-B:Assigning proofs to meaningful programs. In iFM. (Invited paper, Submitted),2013.
[7]J.-R. Abrial, M. J. Butler, S. Hallerstede, and L. Voisin. A roadmap for the rodin toolset. In ABZ, page 347,2008.
[8]J.-R. Abrial and S. Hallerstede. Refinement, decomposition, and instantiation of discrete models:Application to Event-B. Fundam. Inform.,77(1-2):1-28, 2007.
[9]J. R. Abrial and T. S. Hoang. Using design patterns in formal methods:An Event-B approach. In Proceedings of the 5th international colloquium on The-oretical Aspects of Computing, pages 1-2, Berlin, Heidelberg,2008. Springer-Verlag.
[10]J.-R. Abrial, S. A. Schuman, and B. Meyer. Specification language. In On the Construction of Programs, pages 343-410.1980.
[11]J.-R. Abrial, W. Su, and H. Zhu. Formalizing hybrid systems with Event-B. In Proceedings of the Third international conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ'12, pages 178-193, Berlin, Heidelberg,2012. Springer-Verlag.
[12]R. Alur. Formal verification of hybrid systems. In Proceedings of the ninth ACM international conference on Embedded software, EMSOFT'11, pages 273-278, New York, NY, USA,2011. ACM.
[13]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. Theor. Comput. Sci.,138(1):3-34, Feb.1995.
[14]R. Alur, C. Courcoubetis, T. A. Henzinger, and P.-H. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid system-s. In Hybrid Systems, pages 209-229, London, UK, UK,1993. Springer-Verlag.
[15]R. Alur, T. Dang, J. M. Esposito, Y. Hur, F. Ivancic, V. Kumar, I. Lee, P. Mishra, G. J. Pappas, and O.Sokolsky. Hierarchical modeling and analysis of embedded systems. Proceedings of the IEEE,91(1):11-28,2003.
[16]R. Alur, T. Dang, and F. Ivancic. Predicate abstraction for reachability anal-ysis of hybrid systems. ACM Trans. Embedded Comput. Syst,5(1):152-199, 2006.
[17]R. Alur and D. L. Dill. A theory of timed automata. Theor. Comput. Sci, 126(2):183-235,1994.
[18]R. Alur and T. A. Henzinger. Modularity for timed and hybrid systems. In Proceedings of the 8th International Conference on Concurrency Theory, CONCUR'97, pages 74-88, London, UK, UK,1997. Springer-Verlag.
[19]R. Alur, T. A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Trans. Software Eng.,22(3):181-201,1996.
[20]R. Alur, T. A. Henzinger, G. Lafferriere, George, and J. Pappas. Discrete abstractions of hybrid systems. In Proceedings of the IEEE, pages 971-984, 2000.
[21]Animb website, http://www.animb.org/.
[22]N. Ayewah, D. Hovemeyer, J. D. Morgenthaler, J. Penix, and W. Pugh. Using static analysis to find bugs. IEEE Softw.,25(5):22-29, Sept.2008.
[23]R.-J. Back, L. Petre, and I. Porres. Generalizing action systems to hybrid systems. In Proceedings of the 6th International Symposium on Formal Tech-niques in Real-Time and Fault-Tolerant Systems, FTRTFT'00, pages 202-213, London, UK, UK,2000. Springer-Verlag.
[24]R.-J. Back, C. C. Seceleanu, and J. Westerholm. Symbolic simulation of hybrid systems. In Proceedings of the Ninth Asia-Pacific Software Engineering Con-ference, APSEC'02, Washington, DC, USA,2002. IEEE Computer Society.
[25]R. J. R. Back. A calculus of refinements for program derivations. Acta Inf., 25(6):593-624, Aug.1988.
[26]R. J. R. Back. Refinement calculus, part ii:parallel and reactive program-s. In Proceedings on Stepwise refinement of distributed systems:models, for-malisms, correctness, REX workshop, pages 67-93, New York, NY, USA,1990. Springer-Verlag New York, Inc.
[27]R. J. R. Back and F. Kurki-Suonio. Distributed cooperation with action sys-tems. ACM Trans. Program. Lang. Syst.,10(4):513-554, Oct.1988.
[28]R. J. R. Back and K. Sere. Superposition refinement of reactive systems. FOR-MAL ASPECTS OF COMPUTING,8:324-346,1993.
[29]C. Baier and J.-P. Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press,2008.
[30]R. Banach, H. Zhu, W. Su, and R. Huang. Formalising the continuous/discrete modeling step. In Refine, pages 121-138,2011.
[31]R. Banach, H. Zhu, W. Su, and X. Wu. Asm and controller synthesis. In ABZ, pages 51-64,2012.
[32]R. Banach, H. Zhu, W. Su, and X. Wu. Continuous asm, and a pacemaker sensing fragment. In ABZ, pages 65-78,2012.
[33]R. Banach, H. Zhu, W. Su, and X. Wu. Continuous behaviour in Event-B:A sketch. In ABZ, pages 349-352,2012.
[34]M. Beeson. Using nonstandard analysis to ensure the correctness of symbolic computations. Int. J. Found. Comput. Sci.,6(3):299-338,1995.
[35]B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and P. Schnoebelen. Systems and Software Verification:Model-Checking Techniques and Tools. Springer Publishing Company, Incorporated,1st edition,2010.
[36]W. W. Bledsoe and A. M. Ballantyne. Automatic proofs of theorems in analysis using nonstandard techniques. J. ACM,24(3):353-374, July 1977.
[37]J. C. Butcher. Numerical Methods for Ordinary Differential Equations. John Wiley and Sons, New York, USA,2003.
[38]L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. ACM Comput. Surv.,17(4):471-523, Dec.1985.
[39]K. M. Chandy. Parallel program design:a foundation. Addison-Wesley Long-man Publishing Co., Inc., Boston, MA, USA,1988.
[40]E. M. Clarke, A. Fehnker, Z. Han, B. H. Krogh, O. Stursberg, and M. Theobald. Verification of hybrid systems based on counterexample-guided abstraction refinement. In TACAS, pages 192-207,2003.
[41]E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model checking. MIT Press, Cambridge, MA, USA,1999.
[42]J. C. Corbett. Modeling and analysis of real-time ada tasking programs. In In Proceedings of the Real-Time Systems Symposium, IEEE Computer, pages 132-141. IEEE Computer Society Press,1994.
[43]A. Deshpande, A. Gollii, and P. Varaiya. Shift:A formalism and a program-ming language for dynamic networks of hybrid automata. In Hybrid Systems, pages 113-133,1996.
[44]Eclipse website, http://www.eclipse.org/.
[45]J. Eker, J. W. Janneck, E. A. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer, S. R. Sachs, and Y. Xiong. Taming heterogeneity-the ptolemy approach. Proceedings of the IEEE,91(1):127-144,2003.
[46]E.Suli. Numerical Solution of Ordinary Differential Equations. Oxford Uni-versity,2010.
[47]L. Euler. Collected Work of L.Euler,11(1913).
[48]J. D. Fleuriot. On the mechanization of real analysis in isabelle/hol. In Pro-ceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'00, pages 145-161, London, UK, UK,2000. Springer-Verlag.
[49]R. Gerber and I. Lee. Guest a layered approach to automating the verification of real-time systems. IEEE Trans. Softw. Eng.,18(9):768-784, Sept.1992.
[50]A. Girard and G. J. Pappas. Approximation metrics for discrete and continu-ous systems. IEEE Trans. Automat. Contr.,52 (5):782-798,2007.
[51]J. Harrison. Theorem proving with the real numbers. CPHC/BCS distinguished dissertations. Springer,1998.
[52]J. Harrison and L. Thery. Reasoning about the reals:The marriage of hoi and maple. In LPAR, pages 351-353,1993.
[53]T. A. Henzinger. The theory of hybrid automata. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS'96, pages 278-Washington, DC, USA,1996. IEEE Computer Society.
[54]T. A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid sys-tems. In CAV, pages 225-238,1995.
[55]T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech:A model checker for hybrid systems. STTT, 1(1-2):110-122,1997.
[56]T. A. Henzinger, B. Horowitz, R. Majumdar, and H. Wong-Toi. Beyond hytech: Hybrid systems analysis using interval numerical methods. In Proceedings of the Third International Workshop on Hybrid Systems:Computation and Control, HSCC'00, pages 130-144, London, UK, UK,2000. Springer-Verlag.
[57]T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, STOC'95, pages 373-382, New York, NY, USA,1995. ACM.
[58]T. S. Hoang and J.-R. Abrial. Event-B decomposition for parallel programs. In ASM, pages 319-333,2010.
[59]T. S. Hoang, A. Fiirst, and J.-R. Abrial. Event-B patterns and their tool sup-port. In Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM'09, pages 210-219, Wash-ington, DC, USA,2009. IEEE Computer Society.
[60]C. A. R. Hoare. Essays in computing science. Prentice-Hall, Inc., Upper Saddle River, NJ, USA,1989.
[61]C. A. R. Hoare. Software pioneers, chapter Proof of correctness of data rep-resentations, pages 385-396. Springer-Verlag New York, Inc., New York, NY, USA,2002.
[62]H. Jifeng. A classical mind, chapter From CSP to hybrid systems, pages 171-189. Prentice Hall International (UK) Ltd., Hertfordshire, UK, UK,1994.
[63]J.M.Henle and E.M.Kleinberg. Infinitesimal Calculus. The MIT Press,1979.
[64]C. B. Jones. Software Development:A Rigorous Approach. Prentice Hall PTR, Upper Saddle River, NJ, USA,1980.
[65]G. Karsai, J. Sztipanovits, A. Ledeczi, and T. Bapty. Model-integrated de-velopment of embedded software. Proceedings of the IEEE,91(1):145-164, 2003.
[66]H. J. Keisler. Foundations of Infinitesimal Calculus. Prindle Weber and Schmidt,1976.
[67]L. Lamport. A fast mutual exclusion algorithm. ACM Trans. Comput. Syst, 5(1):1-11, Jan.1987.
[68]L. Lamport. The temporal logic of actions. ACM Trans. Program. Lang. Syst, 16(3):872-923, May 1994.
[69]M. Leuschel and M. Butler. Prob:an automated analysis toolset for the b method. Int. J. Softw. Tools Technol. Transf.,10(2):185-203, Feb.2008.
[70]M. Leuschel and M. Butler. Prob:an automated analysis toolset for the b method. Int. J. Softw. Tools Technol. Transf.,10(2):185-203, Feb.2008.
[71]M. Leuschel and M. J. Butler. Prob:an automated analysis toolset for the b method. STTT,10(2):185-203,2008.
[72]C. Lewerentz and T. Lindner, editors. Formal Development of Reactive Sys-tems-Case Study Production Cell, London, UK, UK,1995. Springer-Verlag.
[73]W. Lin, M. Wu, Z. Yang, and Z. Zeng. Exact safety verification of hybrid systems using sums-of-squares representation. CoRR, pages-1-1,2011.
[74]J. Liu, N. Zhan, and H. Zhao. Computing semi-algebraic invariants for poly-nomial dynamical systems. In Proceedings of the ninth ACM international conference on Embedded software, EMSOFT'11, pages 97-106, New York, NY, USA,2011. ACM.
[75]N. Lynch, R. Segala, and F. Vaandrager. Hybrid i/o automata. Inf. Comput, 185(1):105-157, Aug.2003.
[76]I. Maamria, M. Butler, A. Edmunds, and A. Rezazadeh. On an extensible rule-based prover for Event-B. In Proceedings of the Second international conference on Abstract State Machines, Alloy, B and Z, ABZ'10, pages 407-407, Berlin, Heidelberg,2010. Springer-Verlag.
[77]O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In REX Workshop, pages 447-484,1991.
[78]Mathworks website, http://www.mathworks.com/.
[79]Modelica website, http://www.modelica.org/.
[80]C. Morgan. Programming from specifications. Prentice-Hall, Inc., Upper Sad-dle River, NJ, USA,1990.
[81]F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA,1999.
[82]T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle/HOL:a proof assistant for higher-order logic. Springer-Verlag, Berlin, Heidelberg,2002.
[83]L. C. Paulson. The foundation of a generic theorem prover. J. Autom. Reason., 5(3):363-397, Sept.1989.
[84]B. C. Pierce. Types and programming languages. MIT Press, Cambridge, MA, USA,2002.
[85]D. Plagge and M. Leuschel. Validating b, z and tla+using prob and kodkod. In FM, pages 372-386,2012.
[86]A. Platzer. Differential dynamic logic for hybrid systems. J. Autom. Reasoning, 41(2):143-189,2008.
[87]A. Platzer. Logical Analysis of Hybrid Systems:Proving Theorems for Complex Dynamics. Springer, Heidelberg,2010.
[88]A. Platzer and E. M. Clarke. Computing differential invariants of hybrid sys-tems as fixedpoints. In CAV, pages 176-189,2008.
[89]A. Platzer and E. M. Clarke. Formal verification of curved flight collision avoid-ance maneuvers:A case study. In Proceedings of the 2nd World Congress on Formal Methods, FM'09, pages 547-562, Berlin, Heidelberg,2009. Springer-Verlag.
[90]S. Prajna and A. Jadbabaie. Safety verification of hybrid systems using barrier certificates. In HSCC, pages 477-492,2004.
[91]S. Ratschan and Z. She. Safety verification of hybrid systems by constrain-t propagation-based abstraction refinement. ACM Trans. Embed. Comput. Syst.,6(1), Feb.2007.
[92]A. M. Robert. Nonstandard Analysis. Dover Publications,2011.
[93]A. Robinson. Non-standard Analysis. Princeton University Press,1996.
[94]Rodin Plug-ins website, http://wiki.event-b.org/index.php/rodin-plug-ins.
[95]Rodin website. http://wiki.event-b.org/index.php/rodin_platform.
[96]E. Rodriguez-carbonell and A. Tiwari. Generating polynomial invariants for hybrid systems. In In HSCC, pages 590-605. Springer,2005.
[97]M. Y. Said, M. J. Butler, and C. F. Snook. Language and tool support for class and state machine refinement in UML-B. In FM, pages 579-595,2009.
[98]S. Sankaranarayanan, H. Sipma, and Z. Manna. Constructing invariants for hybrid systems. In in Hybrid Systems:Computation and Control, LNCS 2993, pages 539-554. Springer-Verlag,2004.
[99]C. F. Snook, V. Savicks, and M. J. Butler. Verification of uml models by translation to UML-B. In FMCO, pages 251-266,2010.
[100]W. Su, J.-R. Abrial, R. Huang, and H. Zhu. From requirements to develop-ment:Methodology and example. In Proceedings of the 14th international conference on Formal Engineering Methods:formal methods and software en-gineering, ICFEM'11, pages 437-455,2011.
[101]W. Su, J.-R. Abrial, and H. Zhu. Complementary methodologies for devel-oping hybrid systems with Event-B. In Proceedings of the 14th internation-al conference on Formal Engineering Methods: formal methods and software engineering, ICFEM'12, pages 230-248, Berlin, Heidelberg,2012. Springer-Verlag.
[102]P. Tabuada. Verification and Control of Hybrid Systems. Springer,2009.
[103]A. van der Schaft and H. Schumacher. An Introduction to Hybrid Dynamical Systems. Springer,2000.
[104]J. Woodcock and J. Davies. Using Z: specification, refinement, and proof. Prentice-Hall, Inc., Upper Saddle River, NJ, USA,1996.
[105]C. Zhou, J. Wang, and A. P. Ravn. A formal description of hybrid systems. In Proceedings of the DIMACS/SYCON workshop on Hybrid systems Ⅲ: verification and control:verification and control, pages 511-530, Secaucus, NJ, USA,1996. Springer-Verlag New York, Inc.
[2]J.-R. Abrial. The B-book:assigning programs to meanings. Cambridge Uni-versity Press, New York, NY, USA,1996.
[3]J.-R. Abrial. Refinement, decomposition and instantiation of discrete models. In Abstract State Machines, pages 17-40,2005.
[4]J.-R. Abrial. Faultless systems:Yes we can! IEEE Computer,42(9):30-36, 2009.
[5]J.-R. Abrial. Modeling in Event-B:System and Software Engineering. Cam-bridge University Press, New York, NY, USA,1st edition,2010.
[6]J.-R. Abrial. From Z to B and then Event-B:Assigning proofs to meaningful programs. In iFM. (Invited paper, Submitted),2013.
[7]J.-R. Abrial, M. J. Butler, S. Hallerstede, and L. Voisin. A roadmap for the rodin toolset. In ABZ, page 347,2008.
[8]J.-R. Abrial and S. Hallerstede. Refinement, decomposition, and instantiation of discrete models:Application to Event-B. Fundam. Inform.,77(1-2):1-28, 2007.
[9]J. R. Abrial and T. S. Hoang. Using design patterns in formal methods:An Event-B approach. In Proceedings of the 5th international colloquium on The-oretical Aspects of Computing, pages 1-2, Berlin, Heidelberg,2008. Springer-Verlag.
[10]J.-R. Abrial, S. A. Schuman, and B. Meyer. Specification language. In On the Construction of Programs, pages 343-410.1980.
[11]J.-R. Abrial, W. Su, and H. Zhu. Formalizing hybrid systems with Event-B. In Proceedings of the Third international conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ'12, pages 178-193, Berlin, Heidelberg,2012. Springer-Verlag.
[12]R. Alur. Formal verification of hybrid systems. In Proceedings of the ninth ACM international conference on Embedded software, EMSOFT'11, pages 273-278, New York, NY, USA,2011. ACM.
[13]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. Theor. Comput. Sci.,138(1):3-34, Feb.1995.
[14]R. Alur, C. Courcoubetis, T. A. Henzinger, and P.-H. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid system-s. In Hybrid Systems, pages 209-229, London, UK, UK,1993. Springer-Verlag.
[15]R. Alur, T. Dang, J. M. Esposito, Y. Hur, F. Ivancic, V. Kumar, I. Lee, P. Mishra, G. J. Pappas, and O.Sokolsky. Hierarchical modeling and analysis of embedded systems. Proceedings of the IEEE,91(1):11-28,2003.
[16]R. Alur, T. Dang, and F. Ivancic. Predicate abstraction for reachability anal-ysis of hybrid systems. ACM Trans. Embedded Comput. Syst,5(1):152-199, 2006.
[17]R. Alur and D. L. Dill. A theory of timed automata. Theor. Comput. Sci, 126(2):183-235,1994.
[18]R. Alur and T. A. Henzinger. Modularity for timed and hybrid systems. In Proceedings of the 8th International Conference on Concurrency Theory, CONCUR'97, pages 74-88, London, UK, UK,1997. Springer-Verlag.
[19]R. Alur, T. A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Trans. Software Eng.,22(3):181-201,1996.
[20]R. Alur, T. A. Henzinger, G. Lafferriere, George, and J. Pappas. Discrete abstractions of hybrid systems. In Proceedings of the IEEE, pages 971-984, 2000.
[21]Animb website, http://www.animb.org/.
[22]N. Ayewah, D. Hovemeyer, J. D. Morgenthaler, J. Penix, and W. Pugh. Using static analysis to find bugs. IEEE Softw.,25(5):22-29, Sept.2008.
[23]R.-J. Back, L. Petre, and I. Porres. Generalizing action systems to hybrid systems. In Proceedings of the 6th International Symposium on Formal Tech-niques in Real-Time and Fault-Tolerant Systems, FTRTFT'00, pages 202-213, London, UK, UK,2000. Springer-Verlag.
[24]R.-J. Back, C. C. Seceleanu, and J. Westerholm. Symbolic simulation of hybrid systems. In Proceedings of the Ninth Asia-Pacific Software Engineering Con-ference, APSEC'02, Washington, DC, USA,2002. IEEE Computer Society.
[25]R. J. R. Back. A calculus of refinements for program derivations. Acta Inf., 25(6):593-624, Aug.1988.
[26]R. J. R. Back. Refinement calculus, part ii:parallel and reactive program-s. In Proceedings on Stepwise refinement of distributed systems:models, for-malisms, correctness, REX workshop, pages 67-93, New York, NY, USA,1990. Springer-Verlag New York, Inc.
[27]R. J. R. Back and F. Kurki-Suonio. Distributed cooperation with action sys-tems. ACM Trans. Program. Lang. Syst.,10(4):513-554, Oct.1988.
[28]R. J. R. Back and K. Sere. Superposition refinement of reactive systems. FOR-MAL ASPECTS OF COMPUTING,8:324-346,1993.
[29]C. Baier and J.-P. Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press,2008.
[30]R. Banach, H. Zhu, W. Su, and R. Huang. Formalising the continuous/discrete modeling step. In Refine, pages 121-138,2011.
[31]R. Banach, H. Zhu, W. Su, and X. Wu. Asm and controller synthesis. In ABZ, pages 51-64,2012.
[32]R. Banach, H. Zhu, W. Su, and X. Wu. Continuous asm, and a pacemaker sensing fragment. In ABZ, pages 65-78,2012.
[33]R. Banach, H. Zhu, W. Su, and X. Wu. Continuous behaviour in Event-B:A sketch. In ABZ, pages 349-352,2012.
[34]M. Beeson. Using nonstandard analysis to ensure the correctness of symbolic computations. Int. J. Found. Comput. Sci.,6(3):299-338,1995.
[35]B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and P. Schnoebelen. Systems and Software Verification:Model-Checking Techniques and Tools. Springer Publishing Company, Incorporated,1st edition,2010.
[36]W. W. Bledsoe and A. M. Ballantyne. Automatic proofs of theorems in analysis using nonstandard techniques. J. ACM,24(3):353-374, July 1977.
[37]J. C. Butcher. Numerical Methods for Ordinary Differential Equations. John Wiley and Sons, New York, USA,2003.
[38]L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. ACM Comput. Surv.,17(4):471-523, Dec.1985.
[39]K. M. Chandy. Parallel program design:a foundation. Addison-Wesley Long-man Publishing Co., Inc., Boston, MA, USA,1988.
[40]E. M. Clarke, A. Fehnker, Z. Han, B. H. Krogh, O. Stursberg, and M. Theobald. Verification of hybrid systems based on counterexample-guided abstraction refinement. In TACAS, pages 192-207,2003.
[41]E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model checking. MIT Press, Cambridge, MA, USA,1999.
[42]J. C. Corbett. Modeling and analysis of real-time ada tasking programs. In In Proceedings of the Real-Time Systems Symposium, IEEE Computer, pages 132-141. IEEE Computer Society Press,1994.
[43]A. Deshpande, A. Gollii, and P. Varaiya. Shift:A formalism and a program-ming language for dynamic networks of hybrid automata. In Hybrid Systems, pages 113-133,1996.
[44]Eclipse website, http://www.eclipse.org/.
[45]J. Eker, J. W. Janneck, E. A. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer, S. R. Sachs, and Y. Xiong. Taming heterogeneity-the ptolemy approach. Proceedings of the IEEE,91(1):127-144,2003.
[46]E.Suli. Numerical Solution of Ordinary Differential Equations. Oxford Uni-versity,2010.
[47]L. Euler. Collected Work of L.Euler,11(1913).
[48]J. D. Fleuriot. On the mechanization of real analysis in isabelle/hol. In Pro-ceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'00, pages 145-161, London, UK, UK,2000. Springer-Verlag.
[49]R. Gerber and I. Lee. Guest a layered approach to automating the verification of real-time systems. IEEE Trans. Softw. Eng.,18(9):768-784, Sept.1992.
[50]A. Girard and G. J. Pappas. Approximation metrics for discrete and continu-ous systems. IEEE Trans. Automat. Contr.,52 (5):782-798,2007.
[51]J. Harrison. Theorem proving with the real numbers. CPHC/BCS distinguished dissertations. Springer,1998.
[52]J. Harrison and L. Thery. Reasoning about the reals:The marriage of hoi and maple. In LPAR, pages 351-353,1993.
[53]T. A. Henzinger. The theory of hybrid automata. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS'96, pages 278-Washington, DC, USA,1996. IEEE Computer Society.
[54]T. A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid sys-tems. In CAV, pages 225-238,1995.
[55]T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech:A model checker for hybrid systems. STTT, 1(1-2):110-122,1997.
[56]T. A. Henzinger, B. Horowitz, R. Majumdar, and H. Wong-Toi. Beyond hytech: Hybrid systems analysis using interval numerical methods. In Proceedings of the Third International Workshop on Hybrid Systems:Computation and Control, HSCC'00, pages 130-144, London, UK, UK,2000. Springer-Verlag.
[57]T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, STOC'95, pages 373-382, New York, NY, USA,1995. ACM.
[58]T. S. Hoang and J.-R. Abrial. Event-B decomposition for parallel programs. In ASM, pages 319-333,2010.
[59]T. S. Hoang, A. Fiirst, and J.-R. Abrial. Event-B patterns and their tool sup-port. In Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM'09, pages 210-219, Wash-ington, DC, USA,2009. IEEE Computer Society.
[60]C. A. R. Hoare. Essays in computing science. Prentice-Hall, Inc., Upper Saddle River, NJ, USA,1989.
[61]C. A. R. Hoare. Software pioneers, chapter Proof of correctness of data rep-resentations, pages 385-396. Springer-Verlag New York, Inc., New York, NY, USA,2002.
[62]H. Jifeng. A classical mind, chapter From CSP to hybrid systems, pages 171-189. Prentice Hall International (UK) Ltd., Hertfordshire, UK, UK,1994.
[63]J.M.Henle and E.M.Kleinberg. Infinitesimal Calculus. The MIT Press,1979.
[64]C. B. Jones. Software Development:A Rigorous Approach. Prentice Hall PTR, Upper Saddle River, NJ, USA,1980.
[65]G. Karsai, J. Sztipanovits, A. Ledeczi, and T. Bapty. Model-integrated de-velopment of embedded software. Proceedings of the IEEE,91(1):145-164, 2003.
[66]H. J. Keisler. Foundations of Infinitesimal Calculus. Prindle Weber and Schmidt,1976.
[67]L. Lamport. A fast mutual exclusion algorithm. ACM Trans. Comput. Syst, 5(1):1-11, Jan.1987.
[68]L. Lamport. The temporal logic of actions. ACM Trans. Program. Lang. Syst, 16(3):872-923, May 1994.
[69]M. Leuschel and M. Butler. Prob:an automated analysis toolset for the b method. Int. J. Softw. Tools Technol. Transf.,10(2):185-203, Feb.2008.
[70]M. Leuschel and M. Butler. Prob:an automated analysis toolset for the b method. Int. J. Softw. Tools Technol. Transf.,10(2):185-203, Feb.2008.
[71]M. Leuschel and M. J. Butler. Prob:an automated analysis toolset for the b method. STTT,10(2):185-203,2008.
[72]C. Lewerentz and T. Lindner, editors. Formal Development of Reactive Sys-tems-Case Study Production Cell, London, UK, UK,1995. Springer-Verlag.
[73]W. Lin, M. Wu, Z. Yang, and Z. Zeng. Exact safety verification of hybrid systems using sums-of-squares representation. CoRR, pages-1-1,2011.
[74]J. Liu, N. Zhan, and H. Zhao. Computing semi-algebraic invariants for poly-nomial dynamical systems. In Proceedings of the ninth ACM international conference on Embedded software, EMSOFT'11, pages 97-106, New York, NY, USA,2011. ACM.
[75]N. Lynch, R. Segala, and F. Vaandrager. Hybrid i/o automata. Inf. Comput, 185(1):105-157, Aug.2003.
[76]I. Maamria, M. Butler, A. Edmunds, and A. Rezazadeh. On an extensible rule-based prover for Event-B. In Proceedings of the Second international conference on Abstract State Machines, Alloy, B and Z, ABZ'10, pages 407-407, Berlin, Heidelberg,2010. Springer-Verlag.
[77]O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In REX Workshop, pages 447-484,1991.
[78]Mathworks website, http://www.mathworks.com/.
[79]Modelica website, http://www.modelica.org/.
[80]C. Morgan. Programming from specifications. Prentice-Hall, Inc., Upper Sad-dle River, NJ, USA,1990.
[81]F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA,1999.
[82]T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle/HOL:a proof assistant for higher-order logic. Springer-Verlag, Berlin, Heidelberg,2002.
[83]L. C. Paulson. The foundation of a generic theorem prover. J. Autom. Reason., 5(3):363-397, Sept.1989.
[84]B. C. Pierce. Types and programming languages. MIT Press, Cambridge, MA, USA,2002.
[85]D. Plagge and M. Leuschel. Validating b, z and tla+using prob and kodkod. In FM, pages 372-386,2012.
[86]A. Platzer. Differential dynamic logic for hybrid systems. J. Autom. Reasoning, 41(2):143-189,2008.
[87]A. Platzer. Logical Analysis of Hybrid Systems:Proving Theorems for Complex Dynamics. Springer, Heidelberg,2010.
[88]A. Platzer and E. M. Clarke. Computing differential invariants of hybrid sys-tems as fixedpoints. In CAV, pages 176-189,2008.
[89]A. Platzer and E. M. Clarke. Formal verification of curved flight collision avoid-ance maneuvers:A case study. In Proceedings of the 2nd World Congress on Formal Methods, FM'09, pages 547-562, Berlin, Heidelberg,2009. Springer-Verlag.
[90]S. Prajna and A. Jadbabaie. Safety verification of hybrid systems using barrier certificates. In HSCC, pages 477-492,2004.
[91]S. Ratschan and Z. She. Safety verification of hybrid systems by constrain-t propagation-based abstraction refinement. ACM Trans. Embed. Comput. Syst.,6(1), Feb.2007.
[92]A. M. Robert. Nonstandard Analysis. Dover Publications,2011.
[93]A. Robinson. Non-standard Analysis. Princeton University Press,1996.
[94]Rodin Plug-ins website, http://wiki.event-b.org/index.php/rodin-plug-ins.
[95]Rodin website. http://wiki.event-b.org/index.php/rodin_platform.
[96]E. Rodriguez-carbonell and A. Tiwari. Generating polynomial invariants for hybrid systems. In In HSCC, pages 590-605. Springer,2005.
[97]M. Y. Said, M. J. Butler, and C. F. Snook. Language and tool support for class and state machine refinement in UML-B. In FM, pages 579-595,2009.
[98]S. Sankaranarayanan, H. Sipma, and Z. Manna. Constructing invariants for hybrid systems. In in Hybrid Systems:Computation and Control, LNCS 2993, pages 539-554. Springer-Verlag,2004.
[99]C. F. Snook, V. Savicks, and M. J. Butler. Verification of uml models by translation to UML-B. In FMCO, pages 251-266,2010.
[100]W. Su, J.-R. Abrial, R. Huang, and H. Zhu. From requirements to develop-ment:Methodology and example. In Proceedings of the 14th international conference on Formal Engineering Methods:formal methods and software en-gineering, ICFEM'11, pages 437-455,2011.
[101]W. Su, J.-R. Abrial, and H. Zhu. Complementary methodologies for devel-oping hybrid systems with Event-B. In Proceedings of the 14th internation-al conference on Formal Engineering Methods: formal methods and software engineering, ICFEM'12, pages 230-248, Berlin, Heidelberg,2012. Springer-Verlag.
[102]P. Tabuada. Verification and Control of Hybrid Systems. Springer,2009.
[103]A. van der Schaft and H. Schumacher. An Introduction to Hybrid Dynamical Systems. Springer,2000.
[104]J. Woodcock and J. Davies. Using Z: specification, refinement, and proof. Prentice-Hall, Inc., Upper Saddle River, NJ, USA,1996.
[105]C. Zhou, J. Wang, and A. P. Ravn. A formal description of hybrid systems. In Proceedings of the DIMACS/SYCON workshop on Hybrid systems Ⅲ: verification and control:verification and control, pages 511-530, Secaucus, NJ, USA,1996. Springer-Verlag New York, Inc.