The design of exception handling is a complex task requiring insight and domain expertise to ensure that potential abnormal conditions are identified and a recovery process is designed to return the system to a safe state. Formal methods can address this complexity, by supporting the analysis of exception handling at the abstract design stages utilising mathematical modelling and proofs. Event-B is a state-based formal method for modelling and verifying the consistency of discrete systems. However it lacks explicit support for analysing the handling of exceptions. In this paper, we use UML-B state machines to support the modelling of normal behaviour assisting the identification and handling of exceptions. This is followed by verification of exception handler recovery mechanisms using the built-in model checker and provers of the Event-B tool-set.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{FathabadiSHTBAS24,
author = {Asieh Salehi Fathabadi and
Colin F. Snook and
Thai Son Hoang and
Robert Thorburn and
Michael J. Butler and
Leonardo Aniello and
Vladimiro Sassone},
editor = {Silvia Bonfanti and
Angelo Gargantini and
Michael Leuschel and
Elvinia Riccobene and
Patrizia Scandurra},
title = {Designing Exception Handling Using Event-B},
booktitle = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14759},
pages = {270--277},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-63790-2\_22},
doi = {10.1007/978-3-031-63790-2\_22},
timestamp = {Thu, 04 Jul 2024 22:05:23 +0200},
biburl = {https://dblp.org/rec/conf/zum/FathabadiSHTBAS24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}