Showing 1–3 of 3 results for author: Bendisposto, J

Symbolic Reachability Analysis of B through ProB and LTSmin

Authors: Jens Bendisposto, Philipp Koerner, Michael Leuschel, Jeroen Meijer, Jaco van de Pol, Helen Treharne, Jorden Whitefield

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… ▽ More 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. △ Less

Submitted 14 March, 2016; originally announced March 2016.

Who watches the watchers: Validating the ProB Validation Tool

Authors: Jens Bendisposto, Sebastian Krings, Michael Leuschel

Abstract: Over the years, ProB has moved from a tool that complemented proving, to a development environment that is now sometimes used instead of proving for applications, such as exhaustive model checking or data validation. This has led to much more stringent requirements on the integrity of ProB. In this paper we present a summary of our validation efforts for ProB, in particular within the context of t… ▽ More Over the years, ProB has moved from a tool that complemented proving, to a development environment that is now sometimes used instead of proving for applications, such as exhaustive model checking or data validation. This has led to much more stringent requirements on the integrity of ProB. In this paper we present a summary of our validation efforts for ProB, in particular within the context of the norm EN 50128 and safety critical applications in the railway domain. △ Less

Submitted 26 April, 2014; originally announced April 2014.

Comments: In Proceedings F-IDE 2014, arXiv:1404.5785

ACM Class: D.2.4; D.2.5

Journal ref: EPTCS 149, 2014, pp. 16-29

A Semantics-Aware Editing Environment for Prolog in Eclipse

Authors: Jens Bendisposto, Ian Endrijautzki, Michael Leuschel, David Schneider

Abstract: In this paper we present a Prolog plugin for Eclipse based upon BE4, and providing many features such as semantic-aware syntax highlighting, outline view, error marking, content assist, hover information, documentation generation, and quick fixes. The plugin makes use of a Java parser for full Prolog with an integrated Prolog engine, and can be extended with further semantic analyses, e.g., base… ▽ More In this paper we present a Prolog plugin for Eclipse based upon BE4, and providing many features such as semantic-aware syntax highlighting, outline view, error marking, content assist, hover information, documentation generation, and quick fixes. The plugin makes use of a Java parser for full Prolog with an integrated Prolog engine, and can be extended with further semantic analyses, e.g., based on abstract interpretation. △ Less

Submitted 12 March, 2009; originally announced March 2009.

Comments: Paper presented at the 18th Workshop on Logic-based Methods in Programming Environments (WLPE2008) (Report-No: WLPE/2008). Paper submitted by a co-editor of the Workshop proceedings

Report number: WLPE/2008/04