Abstract
Static type checking helps catch errors in manipulating variables values early on, and most specification languages, like Event-B, are strongly typed. However, the type system of Event-B language is relatively simple and provides only a way to specify discrete behaviour using Integer type. There is no possibility to model continuous behaviour, which would have helped analyse hybrid systems. More precisely, the Event-B language doesn’t consider in its type-checking system the possibility of defining such behaviours and checking the correctness of the values of the continuous variables within the Event-B models. In this article, we propose to extend the type-checking system of Event-B to include Float variables by specifying a floating point numbers theory using the theory plugin.
This work was supported by a grant from the French national research agency ANR ANR-19-CE25-0010 (EBRP Project https://www.irit.fr/EBRP/).
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
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
- 4.
- 5.
This is why we have defined a power operator with only natural exponents.
- 6.
References
Abrial, J.: The B-book - assigning programs to meanings. Cambridge University Press, Cambridge (1996). https://doi.org/10.1017/CBO9780511624162
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010). https://doi.org/10.1017/CBO9781139195881
Abrial, J., Butler, M.J., Hallerstede, S., Hoang, 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). https://doi.org/10.1007/s10009-010-0145-y
Ait-Sadoune, I., Mohand-Oussaid, L.: Building formal semantic domain model: an Event-B based approach. In: Schewe, K.-D., Singh, N.K. (eds.) MEDI 2019. LNCS, vol. 11815, pp. 140–155. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32065-2_10
Babin, G., Aït-Ameur, Y., Singh, N.K., Pantel, M.: Handling continuous functions in hybrid systems reconfigurations: a formal Event-B development. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 290–296. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_23
Butler, M.: The first twenty-five years of industrial use of the B-method. In: ter Beek, M.H., Ničković, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 189–209. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58298-2_8
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). https://doi.org/10.1007/978-3-642-39698-4_5
Cervelle, J., Gervais, F.: Introducing inductive construction in B with the theory plugin. In: Glässer, U., Creissac Campos, J., Méry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 43–58. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33163-3_4
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Hoboken (1976)
Hoang, T.S., Voisin, L., Salehi, A., Butler, M.J., Wilkinson, T., Beauger, N.: Theory Plug-in for Rodin 3.x. CoRR abs/1701.08625 (2017). http://arxiv.org/abs/1701.08625
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259
Lecomte, T., Burdy, L., Dufour, J.L.: The B method takes up floating-point numbers. In: Embedded Real Time Software and Systems (ERTS2012) (2012)
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46
Rutenkolk, K.: Extending modelchecking with ProB to floating-point numbers and hybrid systems. In: Glässer, U., Creissac Campos, J., Méry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 366–370. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33163-3_27
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Ait-Sadoune, I. (2024). A Floating-Point Numbers Theory for Event-B. In: Mosbah, M., Kechadi, T., Bellatreche, L., Gargouri, F. (eds) Model and Data Engineering. MEDI 2023. Lecture Notes in Computer Science, vol 14396. Springer, Cham. https://doi.org/10.1007/978-3-031-49333-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-031-49333-1_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-49332-4
Online ISBN: 978-3-031-49333-1
eBook Packages: Computer ScienceComputer Science (R0)