The Event-B method is generally used to build models incrementally by integrating high level requirements. However, developing correct systems is not a cakewalk and remains a challenging task. In this paper, we focus on the preliminary steps of the development of safety-critical systems. We investigate how patterns could be used to generate refinements automatically in the context of an Event-B development. Our main concerns are first to simplify the development of such systems by the use of patterns, and second to produce Event-B machines such that the user can choose to refine them additionally.
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{FaresBF23,
author = {Elie Fares and
Jean{-}Paul Bodeveix and
Mamoun Filali},
editor = {Uwe Gl{\"{a}}sser and
Jos{\'{e}} Creissac Campos and
Dominique M{\'{e}}ry and
Philippe A. Palanque},
title = {Pattern-Based Refinement Generation Through Domain Specific Languages},
booktitle = {Rigorous State-Based Methods - 9th International Conference, {ABZ}
2023, Nancy, France, May 30 - June 2, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14010},
pages = {35--42},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-33163-3\_3},
doi = {10.1007/978-3-031-33163-3\_3},
timestamp = {Fri, 02 Jun 2023 21:23:53 +0200},
biburl = {https://dblp.org/rec/conf/zum/FaresBF23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}