Abstract
Changes like failure or loss of QoS are key aspects of hybrid systems that must be handled during their design. Preserving the system state is a common requirement that can be ensured by reconfiguration relying on system substitution. The specification and design of these systems usually rely on continuous functions whereas their implementation is discrete. Moreover, the associated safety properties are characterized by a safety envelope defining safe system states. This paper presents a novel approach for formalizing the system substitution mechanism for hybrid systems, in which the system substitution maintains a safety envelope of the given hybrid system during system failure or switching from one supporting system to another. Proving the correctness of the discrete implementation of the defined reconfiguration mechanism for hybrid systems is a challenging problem. In this purpose, we propose to combine system substitution and incremental system modeling to ensure correct discretization. We rely on the Event-B method and the Rodin Platform with the Theory plug-in to develop the system models and carry out the proofs on dense real numbers.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996). http://ebooks.cambridge.org/ebook.jsf?bid=CBO9780511624162
Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)
Abrial, J.R., Butler, M., Hallerstede, S., Hong, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)
Abrial, J.R., Butler, M., Hallerstede, S., Leuschel, M., Schmalz, M., Voisin, L.: Proposals for mathematical extensions for Event-B. Technical report (2009)
Babin, G., Aït-Ameur, Y., Nakajima, S., Pantel, M.: Refinement and proof based development of systems characterized by continuous functions. In: Li, X., et al. (eds.) SETTA 2015. LNCS, vol. 9409, pp. 55–70. Springer, Heidelberg (2015). doi:10.1007/978-3-319-25942-0_4
Babin, G., Aït-Ameur, Y., Pantel, M.: Formal verification of runtime compensation of web service compositions: a refinement and proof based proposal with Event-B. In: IEEE International Conference on Services Computing, pp. 98–105 (2015)
Babin, G., Aït-Ameur, Y., Pantel, M.: Correct instantiation of a system reconfiguration pattern: a proof and refinement-based approach. In: IEEE International Symposium on High Assurance Systems Engineering (HASE), pp. 31–38 (2016)
Babin, G., Aït-Ameur, Y., Pantel, M.: Trustworthy cyber-physical systems engineering. In: Romanovsky, A., Ishikawa, F. (eds.) A Generic Model for System Substitution. Chapman and Hall/CRC, Boca Raton (2016)
Banach, R., Butler, M., Qin, S., Verma, N., Zhu, H.: Core hybrid Event-B I: single hybrid Event-B machines. Sci. Comput. Program. 105, 92–123 (2015)
Bhattacharyya, A.: Formal modelling and analysis of dynamic reconfiguration of dependable systems. Ph.D. thesis, Newcastle University, January 2013
Butler, M., Abrial, J.R., Banach, R.: From Action Systems to Distributed Systems: The Refinement Approach, chap. Modelling and Refining Hybrid Systems in Event-B and Rodin, pp. 29–42. Chapman and Hall/CRC., April 2016
Butler, M., Maamria, I.: Practical theory extension in Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 67–81. Springer, Heidelberg (2013)
Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transf. 1(1–2), 110–122 (1997). http://dx.doi.org/10.1007/s100090050008
Iftikhar, M.U., Weyns, D.: A case study on formal verification of self-adaptive behaviors in a decentralized system. In: Kokash, N., Ravara, A. (eds.) 11th International Workshop on Foundations of Coordination Languages and Self Adaptation (FOCLASA 2012), EPTCS, vol. 91, pp. 45–62 (2012)
Jastram, M., Butler, M.: Rodin User’s Handbook: Covers Rodin V.2.8. CreateSpace Independent Publishing Platform, USA (2014). ISBN 10: 1495438147, ISBN 13: 9781495438141, http://handbook.event-b.org
Lanoix, A., Dormoy, J., Kouchnarenko, O.: Combining proof and model-checking to validate reconfigurable architectures. Electron. Notes Theor. Comput. Sci. 279(2), 43–57 (2011)
Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems - A Cyber-Physical Systems Approach. LeeSeshia.org, 1.5 edn. (2014). http://leeseshia.org/
Lin, H.: Mission accomplished: an introduction to formal methods in mobile robot motion planning and control. Unmanned Syst. 02(02), 201–216 (2014)
Pereverzeva, I., Troubitsyna, E., Laibinis, L.: A refinement-based approach to developing critical multi-agent systems. Int. J. Crit. Comput.-Based Syst. 4(1), 69–91 (2013)
Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). http://symbolaris.com/lahs/
Rodrigues, R., Liskov, B., Chen, K., Liskov, M., Schultz, D.: Automatic reconfiguration for large-scale reliable storage systems. IEEE Trans. Dependable Secure Comput. 9(2), 145–158 (2012)
Su, W., Abrial, J.R., Zhu, H.: Formalizing hybrid systems with Event-B and the Rodin platform. Sci. Comput. Program. 94, 164–202 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Babin, G., Aït-Ameur, Y., Singh, N.K., Pantel, M. (2016). A System Substitution Mechanism for Hybrid Systems in Event-B. In: Ogata, K., Lawford, M., Liu, S. (eds) Formal Methods and Software Engineering. ICFEM 2016. Lecture Notes in Computer Science(), vol 10009. Springer, Cham. https://doi.org/10.1007/978-3-319-47846-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-47846-3_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47845-6
Online ISBN: 978-3-319-47846-3
eBook Packages: Computer ScienceComputer Science (R0)