We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.SE

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Software Engineering

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

Authors: John Witulski (Heinrich-Heine Universität Düsseldorf), Michael Leuschel (Heinrich-Heine Universität Düsseldorf)
Abstract: 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.
Comments: In Proceedings F-IDE 2014, arXiv:1404.5785
Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
ACM classes: D.2.4
Journal reference: EPTCS 149, 2014, pp. 93-105
DOI: 10.4204/EPTCS.149.9
Cite as: arXiv:1404.6609 [cs.SE]
  (or arXiv:1404.6609v1 [cs.SE] for this version)

Submission history

From: EPTCS [view email]
[v1] Sat, 26 Apr 2014 05:33:17 GMT (290kb,D)

Link back to: arXiv, form interface, contact.