Formal Modelling and Model Checking of a Flood Monitoring and Rescue System: A Case Study of Safety-Critical System
DOI:
https://doi.org/10.21015/vtse.v12i3.1871Abstract
The flood incidents are becoming more often and severe, thus extreme events require efficient and effective means of controlling and saving lives and property. The reason for this paper is to use Formal Modelling and Model Checking to analyse a new safety critical Flood Monitoring and Rescue System (FMRS) that shall form the basis for the efficient response to floods. Employing the TLA+ analysis, which outlines the FMRS’s dynamic behavior and operational specifications comprehensively. It is important to stress that in our work we address one of the most exciting directions of applying formal methods for the first time in collaboration with real-world safety-critical system designers and offer a powerful and transparent systematic approach to verifying safety-critical systems’ correctness, safety, and reliability. The TLA+ specifications are very carefully designed to represent multiple aspects of the FMRS, such as sensor systems, communication interfaces, as well as the rescue activity itself. To this end, we use model checking methodologies in order to assess the system’s compliance with the required safety properties, including timely detection of floods, correct delivery of data, and synchronization of rescue operations. The performed model checking demonstrates the presence of essential information about the system’s potential failure and weaknesses, which can be used for FMRS architecture improvement and development. Thus, this case shows that the best use of formal methods exist not as ad hoc methods for resolving some issues in the development of safety-critical systems, but a structured template that could be applied in other domains where high degree of assurance in the reliability of a system is needed. Besides the novel method for the better future of the field of formal verification, the proposal also sketches functional relevance of integrating the effective and efficient approaches for monitoring floods and emergency rescue operations in real-world contexts.
References
N. Ali, S. Punnekkat, and A. Rauf, "Modeling and safety analysis for collaborative safety-critical systems using hierarchical colored Petri nets," *Journal of Systems and Software*, 2024. DOI: https://doi.org/10.1016/j.jss.2024.111958
M. Dansarie, "Security issues in special-purpose digital radio communication systems: A systematic review," *IEEE Access*, vol. 19, 2024. DOI: https://doi.org/10.1109/ACCESS.2024.3420091
M. Z. Baig, K. Lagdami, and M. Mejia Jr, "Enhancing maritime safety: A comprehensive review of challenges and opportunities in the domestic ferry sector," *Maritime Technology and Research*, 2024. DOI: https://doi.org/10.33175/mtr.2024.268911
F. Benamara, A. Mari, R. Meunier, and V. Moriceau, "Digging communicative intentions: The case of crises events," *Dialogue & Discourse*, 2024. DOI: https://doi.org/10.5210/dad.2024.101
M. Poursoltan, "Methodological and operational framework for the validation and improvement of cyber-physical and human systems based on modeling and simulation," *theses.hal.science*, 2023.
M. Blais and M. A. Akhloufi, "Drone swarm coordination using reinforcement learning for efficient wildfires fighting," *SN Computer Science*, 2024. DOI: https://doi.org/10.1007/s42979-024-02650-6
D. Corsi, D. Camponogara, and A. Farinelli, "Aquatic navigation: A challenging benchmark for deep reinforcement learning," *arXiv preprint arXiv:2405.20534*, 2024.
J. Crask, *Business Continuity Management: A Practical Guide to Organization Resilience and ISO 22301*, books.google.com, 2024.
T. Jesus, P. Portugal, D. Costa, and F. Vasques, "Reliability and detectability of emergency management systems in smart cities under common cause failures," *Sensors*, 2024. DOI: https://doi.org/10.3390/s24092955
Y. Liu, X. Ma, W. Qiao, and B. Han, "A systematic methodology for resilience evaluation of ship operation in arctic waters combining fram and extended bn," *Available at SSRN 4745705*, 2024. DOI: https://doi.org/10.2139/ssrn.4745705
C. Erbayat, "Investigation of nonlinear interactions causing the major coal mine accidents in Türkiye using system dynamics modeling," *open.metu.edu.tr*, 2024.
A. Hoenig, K. Roy, Y. Acquaah, S. Yi, and S. Desai, "Explainable AI for cyber-physical systems: Issues and challenges," *IEEE Access*, 2024. DOI: https://doi.org/10.1109/ACCESS.2024.3395444
A. H. El-Kady, S. Halim, M. M. El-Halwagi, and F. Khan, "Analysis of safety and security challenges and opportunities related to cyber-physical systems," *Process Safety and Environmental Protection*, 2023. DOI: https://doi.org/10.1016/j.psep.2023.03.012
B. He, Z. Xu, F. Markert, J. Zhao, E. Xie, and Q. Liu, "Incorporating trenchless technology research," *Tunnelling and Underground Space Technology*, 2024.
E. Stefana, M. Ramos, and N. Paltrinieri, "Machine learning-based literature review on the concept of safety barriers against hazardous events," *Available at SSRN 4863735*, 2024. DOI: https://doi.org/10.2139/ssrn.4863735
M. Elapolu, R. Rai, D. J. Gorsich, D. Rizzo, and S. Rapp, "Blockchain technology for requirement traceability in systems engineering," *Information Systems*, 2024. DOI: https://doi.org/10.1016/j.is.2024.102384
H. Sheng, G. Chen, X. Li, J. Men, Q. Xu, and L. Zhou, "A novel unmanned aerial vehicle driven real-time situation awareness for fire accidents in chemical tank farms," *Journal of Loss Prevention in the Process Industries*, 2024. DOI: https://doi.org/10.1016/j.jlp.2024.105357
Z. Mabrek, "IoT network dynamic clustering and communication for surveillance UAV’s," *dspace.univ-guelma.dz*, 2024.
J. Kamberaj, S. Aebi, and A. Hauri, "Trend analysis civil protection 2035 uncertainties, challenges and opportunities," *CSS Risk and Resilience Reports*, 2024.
M. A. Imran, M. Zennaro, and O. R. Popoola, "Exploring the boundaries of connected systems: Communications for hard-to-reach areas and extreme conditions," *Proceedings of the IEEE*, 2024. DOI: https://doi.org/10.1109/JPROC.2024.3402265
E. Yoeyen, "Architecture of safety-critical applications running in the public cloud," *klu edo.ub.rptu.de*, 2023.
N. Ventikos, P. Sotiralis, M. Annetis, *et al.*, "The development and demonstration of an enhanced risk model for the evacuation process of large passenger vessels," *Journal of Marine Science and Engineering*, 2023. DOI: https://doi.org/10.3390/jmse11010084
A. Tubis, H. Poturaj, K. Dereń, and A. Żurek, "Risks of drone use in light of literature studies," *Sensors*, 2024. DOI: https://doi.org/10.3390/s24041205
Z. Liu, J. Yin, R. Liu, and A. D’Ariano, "Vulnerability assessment and optimization of urban rail systems against extreme perturbations: A case study on the Zhengzhou metro flooding," *Available at SSRN 4845235*, 2024. DOI: https://doi.org/10.2139/ssrn.4845235
R. L. Rose, S. R. Mugi, and J. H. Saleh, "Accident investigation and lessons not learned: Accimap analysis of successive tailings dam collapses in Brazil," *Reliability Engineering & System Safety*, 2023. DOI: https://doi.org/10.1016/j.ress.2023.109308
D. Shinar and E. Hauer, "Crash causation, countermeasures, and policy–editorial," *Accident Analysis & Prevention*, 2024. DOI: https://doi.org/10.1016/j.aap.2024.107543
S. Sanusi, S. Paul, and A. Muhammad, *Internet of Green Things (IoGT) for Carbon-Free Economy*, books.google.com, 2024.
C. Rossi, A. Frisiello, and G. Marucco, *A DRM solution for professionals and citizens*, Wiley Online Library, 2024. DOI: https://doi.org/10.1002/9781119741374.ch13
N. G. Leveson, *An Introduction to System Safety Engineering*, books.google.com, 2023.
H. Idoudi, "Dynamic population evacuation," *theses.hal.science*, 2024.
U. Z. A. Hamid, C. Roth, J. Nickerson, K. Lyytinen, and J. L. King, *Vehicle Experience and Human Interaction: Vol. 1*, sae.org, 2024.
A. Hulme, N. A. Stanton, G. H. Walker, and P. Waterson, "Testing the reliability of accident analysis methods: a comparison of accimap, stamp-cast and accinet," *Ergonomics*, 2024. DOI: https://doi.org/10.1080/00140139.2023.2240048
W. Hunt, S. D. Ramchurn, and M. D. Soorati, "A survey of language-based communication in robotics," *arXiv preprint arXiv:2406.04086*, 2024.
M. Krichen and M. S. Abdalzaher, "Advances in AI and drone-based natural disaster management: A survey," in *2023 IEEE International Conference on Computer Systems and Applications (AICCSA)*, ieeexplore.ieee.org, 2023. DOI: https://doi.org/10.1109/AICCSA59173.2023.10479345
A. Förster, J. Dede, A. Könsgen, and K. Kuladinithi, "A beginner’s guide to infrastructure-less networking concepts," *IET Communications*, 2024. DOI: https://doi.org/10.1049/ntw2.12094
M. Kabir, J. Jim, and Z. Istenes, "Fusion-enhanced terrain detection and segmentation for autonomous vehicle navigation: A state-of-the-art systematic review," *Available at SSRN 4797592*, 2024. DOI: https://doi.org/10.2139/ssrn.4797592
Y. R. Mittal, "A simulation study to analyse the impact of V2X communication on the emergency vehicle response time," *opus4.kobv.de*, 2024.
Downloads
Published
How to Cite
Issue
Section
License
Authors who publish with this journal agree to the following terms:
- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License (CC-By) that allows others to share the work with an acknowledgment of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).
This work is licensed under a Creative Commons Attribution License CC BY
