Abstract
For the ABZ2024 conference, the proposed case study consists of modelling an adaptive outdoor mechanical lung ventilation system. The mechanical lung ventilator is intended to provide ventilation support for patients that are in intensive therapy and that require mechanical ventilation. The system under study is made up of two main software components: the graphical user interface (GUI) and the controller, this paper introduces a model for the controller part of the software system using Timed Algebraic State-Transition Diagrams (TASTD). TASTD is an extension of Algebraic State-Transition Diagrams (ASTD) providing timing operators to express timing constraints. The specification makes extensive use of the TASTD modularity capabilities, thanks to its algebraic approach, to model the behaviour of different sensors and actuators separately. We validate our specification using the cASTD compiler, which translates the TASTD specification into a C++ program. This generated program can be executed in simulation mode to manually update the system clock to check timing constraints. The model is executed on the test sequences provided with the case study. The advantages of having modularisation, orthogonality, abstraction, hierarchy, real-time, and graphical representation in one notation are highlighted with the proposed model.
Supported by Public Safety Canada’s Cyber Security Cooperation Program (CSCP) and NSERC (Natural Sciences and Engineering Research Council of Canada).
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
References
Abrial, J.: Modeling in Event-B. Cambridge University Press, Cambridge (2010)
André, C.: Syntax and Semantics of the Clock Constraint Specification Language (CCSL). Research Report RR-6925, INRIA (2009). https://inria.hal.science/inria-00384077
de Azevedo Oliveira, D., Frappier, M.: TASTD: a real-time extension for ASTD. In: Glässer, U., Creissac Campos, J., Méry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 142–159. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33163-3_11
de Azevedo Oliveira, D., Frappier, M.: Technical report 27 - Extending ASTD with real-time (2023). https://github.com/DiegoOliveiraUDES/astd-tech-report-27
Bonfanti, S., Gargantini, A.: The mechanical lung ventilator case study. In: Rigorous State-Based Methods 10th International Conference, ABZ 2024, Bergamo, Italy, 25–28 June 2024, Proceedings, LNCS, vol. 14759. Springer (2024)
Frappier, M.: ASTD support tools repo (2023). https://github.com/DiegoOliveiraUDES/ASTD-tools. Accessed 26 Jan 2024
Gargantini, A.: SCENARIO VERS 1.5 (2023). https://github.com/foselab/abz2024_casestudy_MLV/blob/main/scenarios_v_1_5.pdf
Ndouna, A.R., Frappier, M.: Case Study ABZ 2024 TASTD Model (2024). https://github.com/ndounalex/casestudyABZ2024-tastdmodel
Nganyewou Tidjon, L., Frappier, M., Leuschel, M., Mammar, A.: Extended algebraic state-transition diagrams. In: 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 146–155. Melbourne, Australia (2018)
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.
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Rodrigue Ndouna, A., Frappier, M. (2024). Modelling a Mechanical Lung Ventilation System Using TASTD. 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_26
Download citation
DOI: https://doi.org/10.1007/978-3-031-63790-2_26
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)