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/).
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)