University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Symbolic Reachability Analysis of B through ProB and LTSmin

Bendisposto, J, Koerner, P, Leuschel, M, Meijer, J, Pol, JVD, Treharne, H and Whitefield, J (2016) Symbolic Reachability Analysis of B through ProB and LTSmin Integrated Formal Methods (LNCS), 9681. pp. 275-291.

[img] Text
1603 04401v1.pdf - Author's Original
Restricted to Repository staff only until 24 May 2017.
Available under License : See the attached licence file.

Download (947kB)
[img]
Preview
Text (licence)
SRI_deposit_agreement.pdf
Available under License : See the attached licence file.

Download (33kB) | Preview

Abstract

We present a symbolic reachability analysis approach for B that can provide a significant speedup over traditional explicit state model checking. The symbolic analysis is implemented by linking ProB to LTSmin, a high-performance language independent model checker. The link is achieved via LTSmin's PINS interface, allowing ProB to benefit from LTSmin's analysis algorithms, while only writing a few hundred lines of glue-code, along with a bridge between ProB and C using ZeroMQ. ProB supports model checking of several formal specification languages such as B, Event-B, Z and TLA. Our experiments are based on a wide variety of B-Method and Event-B models to demonstrate the efficiency of the new link. Among the tested categories are state space generation and deadlock detection; but action detection and invariant checking are also feasible in principle. In many cases we observe speedups of several orders of magnitude. We also compare the results with other approaches for improving model checking, such as partial order reduction or symmetry reduction. We thus provide a new scalable, symbolic analysis algorithm for the B-Method and Event-B, along with a platform to integrate other model checking improvements via LTSmin in the future.

Item Type: Article
Subjects : subj_Computing
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
AuthorsEmailORCID
Bendisposto, JUNSPECIFIEDUNSPECIFIED
Koerner, PUNSPECIFIEDUNSPECIFIED
Leuschel, MUNSPECIFIEDUNSPECIFIED
Meijer, JUNSPECIFIEDUNSPECIFIED
Pol, JVDUNSPECIFIEDUNSPECIFIED
Treharne, HUNSPECIFIEDUNSPECIFIED
Whitefield, JUNSPECIFIEDUNSPECIFIED
Date : 14 March 2016
Identification Number : 10.1007/978-3-319-33693-0_18
Copyright Disclaimer : The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-33693-0_18 This is a arXiv version of the work.
Uncontrolled Keywords : cs.SE, cs.SE
Related URLs :
Depositing User : Symplectic Elements
Date Deposited : 24 May 2016 08:23
Last Modified : 11 Nov 2016 17:37
URI: http://epubs.surrey.ac.uk/id/eprint/810795

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800