Abstract
In this paper, we use NASA’s Formal Requirements Elicitation Tool (FRET) and the Event-B formal method to model and verify the requirements for the ABZ 2024 case study, the Mechanical Lung Ventilator. We use the FRET requirements to guide the development of a formal design model in Event-B. We provide details about the artefacts produced and reflect on our experience of using these tools in this case study. We focus on the Functional and Controller requirements for the system, as given in the case study documentation. This paper provides a first step towards using Event-B as part of a FRET-guided verification workflow in a large case study.
All authors (listed alphabetically by surname) contributed equally to this work. This work was partially supported by the Royal Academy of Engineering and EPSRC grant EP/Y001532/1, as well as Maynooth University’s Hume Doctoral Award.
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.
ABZ 2024 Case Study: https://abz-conf.org/case-study/abz24/.
- 2.
FRET GitHub Repository: https://github.com/NASA-SW-VnV/fret.
- 3.
Mechanical Lung Ventilator Repository: https://github.com/foselab/abz2024_casestudy_MLV.
- 4.
FRET and Event-B artefacts: https://github.com/mariefarrell/abz2024.
References
Abba, A., et al.: The novel mechanical ventilator Milano for the Covid-19 pandemic. Phys. Fluids 33(3) (2021)
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.-R., Butler, M., 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. Transfer 12(6), 447–466 (2010)
Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fund. Inform. 77(1–2), 1–28 (2007)
Arcaini, P., Bombarda, A., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: The ASMETA approach to safety assurance of software systems. In: Raschke, A., Riccobene, E., Schewe, K.-D. (eds.) Logic, Computation and Rigorous Methods. LNCS, vol. 12750, pp. 215–238. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-76020-5_13
Banach, R.: The landing gear case study in hybrid Event-B. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 126–141. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07512-9_9
Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: Compositional simulation of abstract state machines for safety critical systems. In: Tapia Tarifa, S.L., Proenca, J. (eds.) FACS 2022. LNCS, vol. 13712, pp. 3–19. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-20872-0_1
Bonfanti, S., Riccobene, E., Santandrea, D., Scandurra, P.: Modeling the MVM-adapt system by compositional I/O abstract state machines. In: Glässer, U., Creissac Campos, J., Méry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 107–115. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33163-3_8
Bonivento, W., Gargantini, A., Krücken, R., Razeto, A.: The mechanical ventilator Milano. Nucl. Phys. News 31(3), 30–33 (2021)
Bourbouh, H., et al.: Integrating formal verification and assurance: an inspection rover case study. In: Dutle, A., Moscato, M.M., Titolo, L., Muñoz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 53–71. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-76384-8_4
Cansell, D., Méry, D., Rehm, J.: Time constraint patterns for Event B development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 140–154. Springer, Heidelberg (2006). https://doi.org/10.1007/11955757_13
Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: a mode-aware contract language for reactive systems. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 347–366. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41591-8_24
Farrell, M., Luckcuck, M., Sheridan, O., Monahan, R.: FRETting about requirements: formalised requirements for an aircraft engine controller. In: Gervasi, V., Vogelsang, A. (eds.) REFSQ 2022. LNCS, vol. 13216, pp. 96–111. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-98464-9_9
Farrell, M., Mavrakis, N., Ferrando, A., Dixon, C., Gao, Y.: Formal modelling and runtime verification of autonomous grasping for active debris removal. Front. Robot. AI (2022)
Farrell, M., Monahan, R., Power, J.F.: Building specifications in the Event-B institution. Logical Methods Comput. Sci. 18 (2022)
Giannakopoulou, D., Mavridou, A., Rhein, J., Pressburger, T., Schumann, J., Shi, N.: Formal requirements elicitation with FRET. In: International Conference on Requirements Engineering: Foundation for Software Quality (2020)
Hallerstede, S.: On the purpose of Event-B proof obligations. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 125–138. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87603-8_11
Hoang, T.S., Snook, C., Ladenberger, L., Butler, M.: Validating the requirements and design of a hemodialysis machine using iUML-B, BMotion studio, and co-simulation. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 360–375. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_31
Hoang, T.S., Snook, C., Salehi, A., Butler, M., Ladenberger, L.: Validating and verifying the requirements and design of a Haemodialysis machine using the Rodin toolset. Sci. Comput. Program. 158, 122–147 (2018)
Kiss, T., Jánosi-Rancz, K.T.: Developing railway interlocking systems with session types and Event-B. In: International Symposium on Applied Computational Intelligence and Informatics, SACI, pp. 93–98. IEEE (2016)
Ladenberger, L., Hansen, D., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. Int. J. Softw. Tools Technol. Transfer 19, 187–203 (2017)
Luckcuck, M., Farrell, M., Sheridan, O., Monahan, R.: A methodology for developing a verifiable aircraft engine controller from formal requirements. In: IEEE Aerospace Conference, pp. 1–12 (2022)
Mammar, A., Laleau, R.: Modeling a landing gear system in Event-B. Int. J. Softw. Tools Technol. Transfer 19, 167–186 (2017)
Mammar, A., Leuschel, M.: Modeling and verifying an arrival manager using Event-B. In: Glässer, U., Creissac Campos, J., Méry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 321–339. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33163-3_24
Mavridou, A., et al.: The ten lockheed martin cyber-physical challenges: formalized, analyzed, and explained. In: Proceedings of the 28th IEEE International Requirements Engineering Conference (2020)
Perez, I., Mavridou, A., Pressburger, T., Goodloe, A., Giannakopoulou, D.: Automated translation of natural language requirements to runtime monitors. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 387–395. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_21
Schneider, S., Treharne, H., Wehrheim, H.: The behavioural semantics of Event-B refinement. Formal Aspects Comput. 26, 251–280 (2014)
Sheridan, O.: Exploring a methodology for formal verification of safety-critical systems. In: Glässer, U., Creissac Campos, J., Méry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 361–365. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33163-3_26
Sheridan, O., Monahan, R., Luckcuck, M.: A requirements-driven methodology: formal modelling and verification of an aircraft engine controller. In: ter Beek, M.H., Monahan, R. (eds.) IFM 2022. LNCS, vol. 13274, pp. 352–356. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-07727-2_21
Snook, C., Butler, M.: UML-B and Event-B: an integration of languages and tools. In: IASTED International Conference on Software Engineering, pp. 336–341 (2008)
Sommerville, I.: Software Engineering. International Computer Science Series. Addison-Wesley (1982)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Ethics declarations
Competing Interests
The author(s) has no competing interests to declare that are relevant to the content of this manuscript.
A Formalised Requirements
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Farrell, M., Luckcuck, M., Monahan, R., Reynolds, C., Sheridan, O. (2024). FRETting and Formal Modelling: A Mechanical Lung Ventilator. In: Bonfanti, S., Gargantini, A., Leuschel, M., Riccobene, E., Scandurra, P. (eds) Rigorous State-Based Methods. ABZ 2024. Lecture Notes in Computer Science, vol 14759. Springer, Cham. https://doi.org/10.1007/978-3-031-63790-2_28
Download citation
DOI: https://doi.org/10.1007/978-3-031-63790-2_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-63789-6
Online ISBN: 978-3-031-63790-2
eBook Packages: Computer ScienceComputer Science (R0)