We argue that B is a good language to conveniently express a wide range of constraint satisfaction problems. We also show that some problems can be solved quite effectively by the ProB tool. We illustrate our claim on several examples, such as the jobs puzzle - for which we solve the challenge set out by Shapiro. Here we show that the B formalization is both very close to the natural language specification and can still be solved efficiently by ProB. Our approach is particularly interesting when a high assurance of correctness is required. Indeed, compared to other existing approaches and tools, validation and double checking of solutions is available for ProB and formal proof can be applied to establish important properties or provide an unambiguous semantics to the problem specification.
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{LeuschelS14,
author = {Michael Leuschel and
David Schneider},
editor = {Yamine A{\"{\i}}t Ameur and
Klaus{-}Dieter Schewe},
title = {Towards {B} as a High-Level Constraint Modelling Language - Solving
the Jobs Puzzle Challenge},
booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International
Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8477},
pages = {101--116},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-662-43652-3\_8},
doi = {10.1007/978-3-662-43652-3\_8},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/LeuschelS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}