2014/04/26 by John Witulski, Michael Leuschel
Computer Science · #cs.SE #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.149.9
published as EPTCS 149, 2014, pp. 93-105 · In Proceedings F-IDE 2014, arXiv:1404.5785
arxiv created 2014/04/26 · arxiv updated 2014/04/29
We present the implementation of pyB, a predicate - and expression - checker for the B language. The tool is to be used for a secondary tool chain for data validation and data generation, with ProB being used in the primary tool chain. Indeed, pyB is an independent cleanroom-implementation which is used to double-check solutions generated by ProB, an animator and model-checker for B specifications. One of the major goals is to use ProB together with pyB to generate reliable outputs for high-integrity safety critical applications. Although pyB is still work in progress, the ProB/pyB toolchain has already been successfully tested on various industrial B machines and data validation tasks.