research-article

Event-B Hybridation: A Proof and Refinement-based Framework for Modelling Hybrid Systems

Authors:

Guillaume Dupont,

Yamine Ait-Ameur,

Neeraj Kumar Singh,

Marc PantelAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 20, Issue 4

Article No.: 35, Pages 1 - 37

https://doi.org/10.1145/3448270

Published: 13 May 2021 Publication History

Abstract

Hybrid systems are complex systems where a software controller interacts with a physical environment, usually named a plant, through sensors and actuators. The specification and design of such systems usually rely on the description of both continuous and discrete behaviours. From complex embedded systems to autonomous vehicles, these systems became quite common, including in safety critical domains. However, their formal verification and validation as a whole is still a challenge.

To address this challenge, this article contributes to the definition of a reusable and tool supported formal framework handling the design and verification of hybrid system models that integrate both discrete (the controller part) and continuous (the plant part) behaviours. This framework includes the development of a process for defining a class of basic theories and developing domain theories and then the use of these theories to develop a generic model and system-specific models. To realise this framework, we present a formal proof tool chain, based on the Event-B correct-by-construction method and its integrated development environment Rodin, to develop a set of theories, a generic model, proof processes, and the required properties for designing hybrid systems in Event-B.

Our approach relies on hybrid automata as basic models for such systems. Discrete and continuous variables model system states and behaviours are given using discrete state changes and continuous evolution following a differential equation. The proposed approach is based on refinement and proof using the Event-B method and the Rodin toolset. Two case studies borrowed from the literature are used to illustrate our approach. An assessment of the proposed approach is provided for evaluating its extensibility, effectiveness, scalability, and usability.

References

[1]

Jean-Raymond Abrial. 1996. The B-Book: Assigning Programs to Meanings. Cambridge University Press.

Digital Library

[2]

Jean-Raymond Abrial. 2010. Modeling in Event-B: System and Software Engineering (1st ed.). Cambridge University Press, New York, NY.

Digital Library

[3]

Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Michael Leuschel, Matthias Schmalz, and Laurent Voisin. 2009. Proposals for Mathematical Extensions for Event-B. Technical Report.

[4]

Ilge Akkaya, Patricia Derler, Shuhei Emoto, and Edward Ashford Lee. 2016. Systems engineering for industrial cyber-physical systems using aspects. Proc. IEEE 104, 5 (May 2016), 997--1012.

[5]

Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. 1995. The algorithmic analysis of hybrid systems. Theor. Comp. Sci. 138, 1 (1995), 3--34. Hybrid Systems.

Digital Library

[6]

James M. Anderson, Kalra Nidhi, Karlyn D. Stanley, Paul Sorensen, Constantine Samaras, and Oluwatobi A. Oluwatola. 2014. Autonomous Vehicle Technology: A Guide for Policymakers. Rand Corporation.

[7]

Manamiary Bruno Andriamiarina, Dominique Méry, and Neeraj Kumar Singh. 2013. Integrating proved state-based models for constructing correct distributed algorithms. In Proceedings of the 10th International Conference on Integrated Formal Methods (IFM’13). 268--284.

[8]

N. Aréchiga, S. M. Loos, A. Platzer, and B. H. Krogh. 2012. Using theorem provers to guarantee closed-loop system properties. In Proceedings of the 2012 American Control Conference. 3573--3580.

[9]

Eugene Asarin, Thao Dang, and Oded Maler. 2002. The d/dt tool for verification of hybrid systems. In Computer Aided Verification, Ed Brinksma and Kim Guldstrand Larsen (Eds.). Springer, Berlin, 365--370.

[10]

Guillaume Babin, Yamine Aït-Ameur, Neeraj Kumar Singh, and Marc Pantel. 2016. A system substitution mechanism for hybrid systems in Event-B. In Formal Methods and Software Engineering, Kazuhiro Ogata, Mark Lawford, and Shaoying Liu (Eds.), Lecture Notes in Computer Science, Vol. 10009. Springer International Publishing, Cham, 106--121.

[11]

Ralph-Johan Back, Luigia Petre, and Ivan Porres. 2000. Generalizing action systems to hybrid systems. In Formal Techniques in Real-Time and Fault-Tolerant Systems, Mathai Joseph (Ed.). Springer, Berlin, 202--213.

[12]

Ralph-Johan Back, Luigia Petre, and Ivan Porres. 2001. Continuous action systems as a model for hybrid systems. Nord. J. Comput. 8, 1 (2001), 2--21.

Digital Library

[13]

Frédéric Badeau and Arnaud Amelot. 2005. Using B as a high level programming language in an industrial project: Roissy VAL. In Proceedings of the Formal Specification and Development in Z and B (ZB’05), Helen Treharne, Steve King, Martin Henson, and Steve Schneider (Eds.). Springer, Berlin, 334--354.

Digital Library

[14]

Richard Banach. 2013. Pliant modalities in hybrid Event-B. In Theories of Programming and Formal Methods, Zhiming Liu, Jim Woodcock, and Huibiao Zhu (Eds.). Lecture Notes in Computer Science, Vol. 8051. Springer, Berlin, 37--53.

[15]

Richard Banach. 2016. Formal refinement and partitioning of a fuel pump system for small aircraft in hybrid Event-B. In Proceedings of the 10th International Symposium on Theoretical Aspects of Software Engineering. 65--72.

[16]

Richard Banach. 2016. Hemodialysis machine in hybrid Event-B. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, and Miklos Biro (Eds.), Lecture Notes in Computer Science. Springer International Publishing, Cham, 376--393.

[17]

Richard Banach, Michael Butler, Shengchao Qin, Nitika Verma, and Huibiao Zhu. 2015. Core hybrid Event-B I: Single hybrid Event-B machines. Science of Computer Programming (2015).

[18]

Richard Banach, Huibiao Zhu, Wen Su, and Runlei Huang. 2011. Formalising the continuous/discrete modeling step. In Proceedings of the 15th International Refinement Workshop (Refine’11)(Electronic Proceedings in Theoretical Computer Science), John Derrick, Eerke A. Boiten, and Steve Reeves (Eds.), Electronic Proceedings in Theoretical Computer Science, Vol. 55. 121--138.

[19]

Richard Banach, Huibiao Zhu, Wen Su, and Xiaofeng Wu. 2012. ASM and controller synthesis. In Abstract State Machines, Alloy, B, VDM, and Z, John Derrick, John Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, and Elvinia Riccobene (Eds.). Lecture Notes in Computer Science, Vol. 7316. Springer, Berlin, 51--64.

[20]

Richard Banach, Huibiao Zhu, Wen Su, and Xiaofeng Wu. 2014. A continuous ASM modelling approach to pacemaker sensing. ACM Trans. Softw. Eng. Methodol. 24, 1, Article 2 (Oct. 2014), 40 pages.

Digital Library

[21]

Patrick Behm, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. 1999. Météor: A Successful Application of B in a Large Project. Springer, Berlin, 369--387.

[22]

Nazim Benaissa and Dominique Méry. 2010. Cryptographic protocols analysis in Event B. In Perspectives of Systems Informatics, Amir Pnueli, Irina Virbitskaite, and Andrei Voronkov (Eds.). Springer, Berlin, 282--293.

[23]

Sarah Benyagoub, Yamine Aït Ameur, Meriem Ouederni, Atif Mashkoor, and Ahmed Medeghri. 2020. Formal design of scalable conversation protocols using Event-B: Validation, experiments, and benchmarks. J. Softw. Evol. Process. 32, 2 (2020).

Digital Library

[24]

Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer Verlag.

[25]

Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. 2014. Trusting computations: A mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68, 3 (2014), 325--352.

Digital Library

[26]

Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. 2015. Coquelicot: A user-friendly library of real analysis for Coq. Math. Comput. Sci. 9, 1 (2015), 41--62.

[27]

Michael Butler, Jean-Raymond Abrial, and Richard Banach. 2016. Modelling and Refining Hybrid Systems in Event-B and Rodin. In From Action Systems to Distributed Systems: The Refinement Approach. Chapman & Hall/CRC, 29--42.

[28]

Michael Butler and Issam Maamria. 2013. Practical theory extension in Event-B. In Theories of Programming and Formal Methods, Zhiming Liu, Jim Woodcock, and Huibiao Zhu (Eds.), Lecture Notes in Computer Science, Vol. 8051. Springer, Berlin, 67--81.

[29]

Michael J. Butler, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, and Laurent Voisin. 2020. The first twenty-five years of industrial use of the B-method. In Proceedings of the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS’20), Maurice H. ter Beek and Dejan Nickovic (Eds.),Lecture Notes in Computer Science, Vol. 12327. Springer, 189--209.

Digital Library

[30]

Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer, Berlin, 258--263.

[31]

Edmund M. Clarke, Orna Grumberg, and Doron Peled. 1999. Model Checking. The MIT Press.

[32]

Armando. W. Colombo, Stamatis Karnouskos, Okyay Kaynak, Yang Shi, and Shen Yin. 2017. Industrial cyberphysical systems: A backbone of the fourth industrial revolution. IEEE Industr. Electr. Mag. 11, 1 (2017), 6--16.

[33]

Nilanjan Dey, Amira S. Ashour, Fuqian Shi, Simon James Fong, and João Manuel Tavares. 2018. Medical cyber-physical systems: A survey. J. Med. Syst. 42, 4 (Apr. 2018), 1--13.

Digital Library

[34]

Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel, and Neeraj Kumar Singh. 2018. Hybrid systems and Event-B: A formal approach to signalised left-turn assist. In New Trends in Model and Data Engineering. Springer International Publishing, 153--158.

[35]

Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel, and Neeraj Kumar Singh. 2018. Proof-based approach to hybrid systems development: Dynamic logic and Event-B. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, Michael Butler, Alexander Raschke, Thai Son Hoang, and Klaus Reichl (Eds.). Springer International Publishing, Cham, 155--170.

[36]

Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel, and Neeraj Kumar Singh. 2020. An Event-B based generic framework for hybrid systems formal modelling. In Proceedings of the 16th International Conference on integrated Formal Methods (iFM’20), Brijesh Dongol and Elena Troubitsyna (Eds.), Lecture Notes in Computer Science. Springer.

Digital Library

[37]

Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel, and Neeraj Kumar Singh. 2020. Formally verified architecture patterns of hybrid systems using proof and refinement with Event-B. In Proceedings of the 7th International Conference on Rigorous State Based Methods, Alexander Rashke and Dominique Méry (Eds.), Lecture Notes in Computer Science, Vol. 12071. Springer, 155--170.

[38]

Guillaume Dupont, Yamine Aït-Ameur, Neeraj K. Singh, Fuyuki Ishikawa, Tsutomu Kobayashi, and Marc Pantel. 2020. Embedding approximation in Event-B: Safe hybrid system design using proof and refinement. In Proceedings of the 22nd International Conference on Formal Engineering Methods (ICFEM’20), Jin Song Dong and Jim McCarthy (Eds.), Lecture Notes in Computer Science, Vol. 12531. Springer, 251--267.

Digital Library

[39]

Guillaume Dupont, Yamine Aït Ameur, Marc Pantel, and Neeraj Kumar Singh. 2019. Handling refinement of continuous behaviors: A proof based approach with Event-B. In Proceedings of the 13th International Symposium on Theoretical Aspects of Software Engineering, Dominique Méry and Shengchao Qin (Eds.). IEEE Computer Society, 9--16.

[40]

Andreas Eggers, Nacim Ramdani, Nedialko Nedialkov, and Martin Fränzle. 2011. Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods. Springer, Berlin, 172--187.

[41]

Janaka Ekanayake, Nick Jenkins, Kithsiri Liyanage, Jianzhong Wu, and Akihiko Yokoyama. 2012. Smart Grid: Technology and Applications (1st ed.). Wiley Publishing.

[42]

Didier Essamé and Daniel Dollé. 2006. B in large-scale projects: The canarsie line CBTC experience. In B 2007: Formal Specification and Development in B, Jacques Julliand and Olga Kouchnarenko (Eds.). Springer, Berlin, 252--254.

[43]

Jean-Christophe Filliâtre and Claude Marché. 2007. The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. Springer, Berlin, 173--177.

[44]

Goran Frehse. 2008. PHAVer: Algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transfer 10, 3 (2008), 263--279.

Digital Library

[45]

Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable verification of hybrid systems. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer, Berlin, 379--395.

Digital Library

[46]

Martin Fränzle, Christian Herde, Tino Teige, Stefan Ratschan, and Tobias Schubert. 2007. Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J. Satisfiabil. Bool. Model. Comput. 1, 3-4 (2007), 209--236.

[47]

Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. 2015. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Proceedings of the 25th International Conference on Automated Deduction, Amy P. Felty and Aart Middeldorp (Eds.), Lecture Notes in Computer Science. Springer International Publishing, 527--538.

[48]

Antoine Girard and George J. Pappas. 2007. Approximate bisimulation relations for constrained linear systems. Automatica 43, 8 (2007), 1307--1317.

Digital Library

[49]

Christoph Grimm, Peter Neumann, and Stefan Mahlknecht. 2014. Embedded Systems for Smart Appliances and Energy Management. Springer.

[50]

Thomas A. Henzinger. 2000. The theory of hybrid automata. In Verification of Digital and Hybrid Systems, M. Kemal Inan and Robert P. Kurshan (Eds.). NATO ASI Series, Vol. 170. Springer, Berlin, 265--292.

[51]

Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. 1997. HyTech: A model checker for hybrid systems. Int. J. Softw. Tools Technol. Transfer 1, 1-2 (1997), 110--122.

Digital Library

[52]

C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice Hall.

Digital Library

[53]

Fabian Immler. 2018. A verified ODE solver and the lorenz attractor. J. Autom. Reason. 61, 1-4 (2018), 73--111.

Digital Library

[54]

Fabian Immler, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin Chen, Marcelo Forets, Luca Geretti, Niklas Kochdumper, David P. Sanders, and Christian Schilling. 2019. ARCH-COMP19 category report: Continuous and hybrid systems with nonlinear dynamics. In Proceedings of the 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi (ARCH’19), Goran Frehse and Matthias Althoff (Eds.), EPiC Series in Computing, Vol. 61. EasyChair, 41--61.

[55]

Fabian Immler, Matthias Althoff, Xin Chen, Chuchu Fan, Goran Frehse, Niklas Kochdumper, Yangge Li, Sayan Mitra, Mahendra Singh Tomar, and Majid Zamani. 2018. ARCH-COMP18 category report: Continuous and hybrid systems with nonlinear dynamics. In Proceedings of the 5th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH@ADHS’18), Goran Frehse, Matthias Althoff, Sergiy Bogomolov, and Taylor T. Johnson (Eds.), EPiC Series in Computing, Vol. 54. EasyChair, 53--70.

[56]

Fabian Immler and Christoph Traut. 2019. The flow of ODEs: Formalization of variational equation and Poincaré map. J. Autom. Reason. 62, 2 (2019), 215--236.

Digital Library

[57]

He Jifeng. 1994. From CSP to hybrid systems. In A Classical Mind. Prentice Hall International (UK) Ltd., 171--189.

[58]

Yanni Kouskoulas, David Renshaw, André Platzer, and Peter Kazanzides. 2013. Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC’13). Association for Computing Machinery, New York, NY, 263--272.

Digital Library

[59]

Linas Laibinis, Elena Troubitsyna, Inna Pereverzeva, Ian Oliver, and Silke Holtmanns. 2016. A formal approach to identifying security vulnerabilities in telecommunication networks. In Formal Methods and Software Engineering, Kazuhiro Ogata, Mark Lawford, and Shaoying Liu (Eds.). Springer International Publishing, Cham, 141--158.

[60]

Edward Ashford Lee. 2014. Constructive Models of Discrete and Continuous Physical Phenomena. Technical Report UCB/EECS-2014-15. EECS Department, University of California, Berkeley.

[61]

Edward Ashford Lee. 2015. The past, present and future of cyber-physical systems: A focus on models. Sensors 15, 3 (2015), 4837.

[62]

Edward Ashford Lee and Sanjit Arunkumar Seshia. 2014. Introduction to Embedded Systems—A Cyber-Physical Systems Approach (1.5 ed.). LeeSeshia.org.

[63]

Jiang Liu, Jidong Lv, Zhao Quan, Naijun Zhan, Hengjun Zhao, Chaochen Zhou, and Liang Zou. 2010. A calculus for hybrid CSP. In Programming Languages and Systems, Kazunori Ueda (Ed.), Lecture Notes in Computer Science,Vol. 6461. Springer, Berlin, 1--15.

[64]

Sarah M. Loos and André Platzer. 2016. Differential refinement logic. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’16). ACM, New York, NY, 505--514.

[65]

Simon Lunel, Benoît Boyer, and Jean-Pierre Talpin. 2017. Compositional proofs in differential dynamic logic dL. In Proceedings of the 17th International Conference on Application of Concurrency to System Design (ACSD’17). IEEE Computer Society, 19--28.

[66]

Simon Lunel, Stefan Mitsch, Benoît Boyer, and Jean-Pierre Talpin. 2019. Parallel composition and modular verification of computer controlled systems in differential dynamic logic. In Proceedings of the 3rd World Congress on Formal Methods: The Next 30 Years (FM’19), Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira (Eds.), Lecture Notes in Computer Science, Vol. 11800. Springer, 354--370.

Digital Library

[67]

Claude Marché. 2007. Jessie: An intermediate language for Java and C verification. In Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification (PLPV’07). ACM, New York, NY, 1--2.

Digital Library

[68]

Larissa Meinicke and Ian J. Hayes. 2006. Continuous action system refinement. In Proceedings of the 8th International Conference on Mathematics of Program Construction (MPC’06). Springer-Verlag, Berlin, 316--337.

[69]

Dominique Méry and Neeraj Kumar Singh. 2011. Analysis of DSR protocol in Event-B. InProceedings of the International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS’11). Springer-Verlag, Berlin, 401--415.

[70]

Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag.

Digital Library

[71]

André Platzer. 2008. Differential dynamic logic for hybrid systems. J. Autom. Reason. 41, 2 (2008), 143--189.

Digital Library

[72]

André Platzer. 2015. A uniform substitution calculus for differential dynamic logic. In Proceedings of the 25th International Conference on Automated Deduction, Amy P. Felty and Aart Middeldorp (Eds.), Lecture Notes in Computer Science. Springe International Publishing, 467--481.

[73]

André Platzer and Edmund M. Clarke. 2009. Formal verification of curved flight collision avoidance maneuvers: A case study. In Proceedings of the Annual Conference on Formal Methods (FM’09), Ana Cavalcanti and Dennis R. Dams (Eds.). Springer, Berlin, 547--562.

[74]

André Platzer and Jan-David Quesel. 2008. KeYmaera: A hybrid theorem prover for hybrid systems. In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR’08), Alessandro Armando, Peter Baumgartner, and Gilles Dowek (Eds.), Lecture Notes in Computer Science, Vol. 5195. Springer, 171--178.

[75]

André Platzer and Jan-David Quesel. 2009. European train control system: A case study in formal verification. In Formal Methods and Software Engineering, Karin Breitman and Ana Cavalcanti (Eds.). Springer, Berlin, 246--265.

[76]

Claudius Ptolemaeus (Ed.). 2014. System Design, Modeling, and Simulation Using Ptolemy II. Ptolemy.org.

[77]

Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer. 2016. How to model and prove hybrid systems with KeYmaera: A tutorial on safety. Int. J. Softw. Tools Technol. Transfer 18, 1 (2016), 67--91.

Digital Library

[78]

Klaus Schwab. 2017. The Fourth Industrial Revolution. Crown Publishing Group, USA.

Digital Library

[79]

Neeraj Kumar Singh. 2013. Using Event-B for Critical Device Software Systems. Springer.

[80]

Neeraj Kumar Singh, Yamine Aït Ameur, Marc Pantel, Arnaud Dieumegard, and Eric Jenn. 2016. Stepwise formal modeling and verification of self-adaptive systems with Event-B. The automatic rover protection case study. In Proceedings of the 21st International Conference on Engineering of Complex Computer Systems (ICECCS’16). 43--52.

[81]

Neeraj Kumar Singh, Hao Wang, Mark Lawford, Thomas Stephen Edward Maibaum, and Alan Wassyng. 2015. Stepwise formal modelling and reasoning of insulin infusion pump requirements. In Proceedings of the Conference on Digital Human Modeling: Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health (DHM’15). 387--398.

[82]

Paulius Stankaitis, Andrei Iliasov, Yamine Ait-Ameur, Tsutomu Kobayashi, Fuyuki Ishikawa, and Alexander Romanovsky. 2019. A refinement based method for developing distributed protocols. In Proceedings of the 2019 IEEE 19th International Symposium on High Assurance Systems Engineering (HASE’19). 90--97.

[83]

Wen Su and Jean-Raymond Abrial. 2014. Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System. Springer International Publishing, 19--35.

[84]

Wen Su and Jean-Raymond Abrial. 2017. Aircraft landing gear system: Approaches with Event-B to the modeling of an industrial system. Int. J. Softw. Tools Technol. Transf. 19, 2 (Apr. 2017), 141--166.

Digital Library

[85]

Wen Su, Jean-Raymond Abrial, and Huibiao Zhu. 2014. Formalizing hybrid systems with Event-B and the Rodin platform. Sci. Comput. Program. 94, 2 (2014), 164--202.

Digital Library

[86]

Sebastian Thrun, Mike Montemerlo, Hendrik Dahlkamp, David Stavens, Andrei Aron, James Diebel, Philip Fong, John Gale, Morgan Halpenny, Gabriel Hoffmann, Kenny Lau, Celia Oakley, Mark Palatucci, Vaughan Pratt, Pascal Stang, Sven Strohband, Cedric Dupont, Lars-Erik Jendrossek, Christian Koelen, Charles Markey, Carlo Rummel, Joe van Niekerk, Eric Jensen, Philippe Alessandrini, Gary Bradski, Bob Davies, Scott Ettinger, Adrian Kaehler, Ara Nefian, and Pamela Mahoney. 2007. Stanley: The Robot That Won the DARPA Grand Challenge. Springer, Berlin, 1--43.

[87]

Shuling Wang, Naijun Zhan, and Liang Zou. 2015. An improved HHL prover: An interactive theorem prover for hybrid systems. In Proceedings of the 17th International Conference on Formal Engineering Methods (ICFEM’15), Michael J. Butler, Sylvain Conchon, and Fatiha Zaïdi (Eds.), Lecture Notes in Computer Science, Vol. 9407. Springer, 382--399.

[88]

Hengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, and Yao Chen. 2014. Formal verification of a descent guidance control program of a lunar lander. In Proceedings of the Annual Conference on Formal Methods (FM’14), Cliff Jones, Pekka Pihlajasaari, and Jun Sun (Eds.). Springer International Publishing, Cham, 733--748.

Digital Library

[89]

Chaochen Zhou, Ji Wang, and Anders P. Ravn. 1996. A formal description of hybrid systems. In Hybrid Systems III, Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag (Eds.), Lecture Notes in Computer Science, Vol. 1066. Springer, Berlin, 511--530.

[90]

Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan, and Yu Liu. 2014. Verifying Chinese train control system under a combined scenario by theorem proving. In Verified Software: Theories, Tools, Experiments, Ernie Cohen and Andrey Rybalchenko (Eds.). Springer, Berlin, 262--280.

[91]

Farah Zoubeyr, Yamine Aït Ameur, Meriem Ouederni, and Abdelkamel Tari. 2017. A correct-by-construction model for asynchronously communicating systems. Int. J. Softw. Tools Technol. Transf. 19, 4 (2017), 465--485.

Digital Library

Cited By

Rivière PSingh NAït-Ameur Y(2024)Reflexive Event-B: Semantics and Correctness the EB4EB FrameworkIEEE Transactions on Reliability10.1109/TR.2022.321964973:2(835-850)Online publication date: Jun-2024
https://doi.org/10.1109/TR.2022.3219649
Wang SJi ZXu XZhan BGao QZhan N(2024)Formally Verified C Code Generation from Hybrid Communicating Sequential Processes2024 ACM/IEEE 15th International Conference on Cyber-Physical Systems (ICCPS)10.1109/ICCPS61052.2024.00018(123-134)Online publication date: 13-May-2024
https://doi.org/10.1109/ICCPS61052.2024.00018
Banach R(2024)Core Hybrid Event-B III: Fundamentals of a reasoning frameworkScience of Computer Programming10.1016/j.scico.2023.103002231(103002)Online publication date: Jan-2024
https://doi.org/10.1016/j.scico.2023.103002
Show More Cited By

Index Terms

Event-B Hybridation: A Proof and Refinement-based Framework for Modelling Hybrid Systems

Recommendations

Towards the Composition of Specifications in Event-B

The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal ...
Core Hybrid Event-B I

Faced with the increasing need for correctly designed hybrid and cyber-physical systems today, the problem of including provision for continuously varying behaviour as well as the usual discrete changes of state is considered in the context of Event-B. ...
Formalizing hybrid systems with Event-B and the Rodin Platform

This paper contains the development of hybrid systems with Event-B and the Rodin Platform. It follows the seminal approach introduced at the turn of the century in Action Systems. Many examples that have been entirely proved with the Rodin Platform ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 20, Issue 4

Special Issue on FDL2019

July 2021

256 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/3458852

Editor:
Tulika Mitra
National University of Singapore, Singapore

Issue’s Table of Contents

Copyright © 2021 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 13 May 2021

Accepted: 01 January 2021

Revised: 01 December 2020

Received: 01 January 2020

Published in TECS Volume 20, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Agence Nationale de la Recherche

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
205
Total Downloads

Downloads (Last 12 months)25
Downloads (Last 6 weeks)3

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Rivière PSingh NAït-Ameur Y(2024)Reflexive Event-B: Semantics and Correctness the EB4EB FrameworkIEEE Transactions on Reliability10.1109/TR.2022.321964973:2(835-850)Online publication date: Jun-2024
https://doi.org/10.1109/TR.2022.3219649
Wang SJi ZXu XZhan BGao QZhan N(2024)Formally Verified C Code Generation from Hybrid Communicating Sequential Processes2024 ACM/IEEE 15th International Conference on Cyber-Physical Systems (ICCPS)10.1109/ICCPS61052.2024.00018(123-134)Online publication date: 13-May-2024
https://doi.org/10.1109/ICCPS61052.2024.00018
Banach R(2024)Core Hybrid Event-B III: Fundamentals of a reasoning frameworkScience of Computer Programming10.1016/j.scico.2023.103002231(103002)Online publication date: Jan-2024
https://doi.org/10.1016/j.scico.2023.103002
Aït-Ameur YBogomolov SDupont GIliasov ARomanovsky AStankaitis P(2023)A Refinement-based Formal Development of Cyber-physical Railway Signalling SystemsFormal Aspects of Computing10.1145/352405235:1(1-1)Online publication date: 12-Jan-2023
https://dl.acm.org/doi/10.1145/3524052
Xu XTalpin JWang SZhan BZhan N(2023)Semantics Foundation for Cyber-physical Systems Using Higher-order UTPACM Transactions on Software Engineering and Methodology10.1145/351719232:1(1-48)Online publication date: 13-Feb-2023
https://dl.acm.org/doi/10.1145/3517192
Mendil IAït-Ameur YSingh NDupont GMéry DPalanque P(2023)Formal domain-driven system development in Event-BJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2022.102798135:COnline publication date: 1-Feb-2023
https://dl.acm.org/doi/10.1016/j.sysarc.2022.102798
Singh NFajge AHalder RAlam M(2023)Formal verification and code generation for solidity smart contractsDistributed Computing to Blockchain10.1016/B978-0-323-96146-2.00028-0(125-144)Online publication date: 2023
https://doi.org/10.1016/B978-0-323-96146-2.00028-0
Rivière PSingh NAït-Ameur YDupont G(2023)Formalising Liveness Properties in Event-B with the Reflexive EB4EB FrameworkNASA Formal Methods10.1007/978-3-031-33170-1_19(312-331)Online publication date: 16-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-33170-1_19
Kobayashi TBondu MIshikawa F(2023)Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B RefinementFormal Methods10.1007/978-3-031-27481-7_30(533-549)Online publication date: 6-Mar-2023
https://dl.acm.org/doi/10.1007/978-3-031-27481-7_30
Riviere PSingh NAit-Ameur Y(2022)EB4EB: A Framework for Reflexive Event-B2022 26th International Conference on Engineering of Complex Computer Systems (ICECCS)10.1109/ICECCS54210.2022.00017(71-80)Online publication date: Mar-2022
https://doi.org/10.1109/ICECCS54210.2022.00017
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View Issue’s Table of Contents