FRETting and Formal Modelling: A Mechanical Lung Ventilator

Farrell, Marie; Luckcuck, Matt; Monahan, Rosemary; Reynolds, Conor; Sheridan, Oisín

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.

Citation

Farrell, M., Luckcuck, M., Monahan, R., Reynolds, C., & Sheridan, O. (2024, June). FRETting and Formal Modelling: A Mechanical Lung Ventilator. Presented at Rigorous State-Based Methods (ABZ 2024), Bergamo, Italy

• Presentation Conference Type: Edited Proceedings
• Conference Name: Rigorous State-Based Methods (ABZ 2024)
• Start Date: Jun 25, 2024
• End Date: Jun 28, 2024
• Acceptance Date: Jun 20, 2024
• Online Publication Date: Jun 20, 2024
• Publication Date: Jun 21, 2024
• Deposit Date: Mar 3, 2025
• Print ISSN: 0302-9743
• Electronic ISSN: 1611-3349
• Publisher: Springer
• Peer Reviewed: Peer Reviewed
• Pages: 360-383
• Series Title: Lecture Notes in Computer Science
• Series Number: 145759
• Series ISSN: 1611-3349
• Book Title: Rigorous State-Based Methods: 10th International Conference, ABZ 2024, Bergamo, Italy, June 25–28, 2024, Proceedings
• ISBN: 9783031637896
• DOI: https://doi.org/10.1007/978-3-031-63790-2_28
• Public URL: https://nottingham-repository.worktribe.com/output/45862811
• Publisher URL: https://link.springer.com/book/10.1007/978-3-031-63790-2
• Additional Information: First Online: 21 June 2024; : The author(s) has no competing interests to declare that are relevant to the content of this manuscript.; Conference Acronym: ABZ; Conference Name: International Conference on Rigorous State-Based Methods; Conference City: Bergamo; Conference Country: Italy; Conference Year: 2024; Conference Start Date: 25 June 2024; Conference End Date: 28 June 2024; Conference Number: 10; Conference ID: abz2024; Conference URL: https://abz-conf.org/site/2024/