Constraint satisfaction and data validation problems can be expressed very elegantly in state-based formal methods such as B. However, is B suited for developing larger applications and are there existing tools that scale for these projects? In this paper, we present our experiences on two real-world data validation projects from different domains which are based on the B language and use ProB as the central validation tool. The first project is the validation of university timetables, and the second project is the validation of railway topologies. Based on these two projects, we present a general structure of a data validation project in B and outline common challenges along with various solutions. We also discuss possible evolutions of the B language to make it (even) more suitable for such projects.
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{HansenSL16,
author = {Dominik Hansen and
David Schneider and
Michael Leuschel},
editor = {Michael J. Butler and
Klaus{-}Dieter Schewe and
Atif Mashkoor and
Mikl{\'{o}}s Bir{\'{o}}},
title = {Using {B} and ProB for Data Validation Projects},
booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9675},
pages = {167--182},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-33600-8\_10},
doi = {10.1007/978-3-319-33600-8\_10},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/HansenSL16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}