Integration of the ProB model checker into Eclipse
Jens Bendisposto · 2006
Writing a formal specification for real-life, industrial problems is a difficult and error prone task, even for experts in formal methods. In the process of specifying a formal model for later refinement and implementation, it is crucial to get approval and feedback from domain experts to avoid the costs of changing a specification at a late point of the development. But understanding formal models written in a specification language like B requires mathematical knowledge a domain expert might not have. In this work we present various improvements to the PROB tool, mainly aimed at making it a better tool for bringing formal methods to industrial developers and domain experts. The main contributions of this work are: 1. A notable recent development in the B world is the RODIN platform , which is an open tool platform based on Eclipse to support Event B, an evolution of B to specify reactive systems. The current version of PROB supports so-called “classical” B and in order to support the new Event B language we needed to integrate PROB into the RODIN/Eclipse platform. Another incentive for this move lay in improving the graphical user interface of the tool, which was originally developed in (and limited by) Tcl/Tk. 2. We changed the B Parser by B. Tatibouet to improve performance in case of syntax errors. Also the B Parser now can directly produce Prolog facts that can be used by PROB. 3. It is important that specifications can be animated in such a way that domain experts can easily validate whether the specification corresponds to their expectations. While PROB allows automated animation, the visualisation may still be difficult to understand for domain experts not versed in formal methods. To overcome this hurdle we have developed a generic Flash-based animation engine which allows to easily develop visualizations for a given specification.