Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB

John Witulski
(Heinrich-Heine Universität Düsseldorf)
Michael Leuschel
(Heinrich-Heine Universität Düsseldorf)

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.

In Catherine Dubois, Dimitra Giannakopoulou and Dominique Méry: Proceedings 1st Workshop on Formal Integrated Development Environment (F-IDE 2014), Grenoble, France, April 6, 2014, Electronic Proceedings in Theoretical Computer Science 149, pp. 93–105.
Published: 26th April 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: