Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
ProB
[go: Go Back, main page]
Please visit the new ProB web site at:

http://www.stups.uni-duesseldorf.de/ProB/

The old pages are still available in case you wish to download a release prior to 1.2.

Old Web Site

The ProB Animator and Model Checker for the B Method

ProB is an animator and model checker for the B-Method (see the B Site Pages or the Formal Methods Virtual Library). It allows fully automatic animation of many B specifications, and can be used to systematically check a specification for errors. ProB is maintained by Michael Leuschel. It is based on research and implementation effort by Michael Leuschel, Michael Butler, Carla Ferreira, Leonid Mikhailov, Edward Turner, Phil Turner, and Laksono Adhianto. Part of the research and development was conducted within the EPSRC funded projects ABCD and iMoc.

The Implementation

ProB was developed using SICStus Prolog (but can be run without a SICStus Prolog license). It uses co-routining and finite domain constraint solving to make animation of B machines possible. The input for ProB is the XML encoding provided by Bruno Tatibouet's jbtools B-to-XML parser.

Features

ProB covers a large part of B, and we are striving towards full coverage. ProB supports B features such as non-deterministic operations, ANY statements, operations with complex arguments, sets, sequences, functions, lambda abstractions, set comprehensions, constants and properties, and many more. It has limited support for multiple machines and refinements.

Download

A first alpha release of ProB has been made available on October 1 2003, with regular updates posted since then. Version 1.1.7 was made available on September 22, 2005.

Several versions of ProB are available for download here. You do not require a SICStus Prolog license to run the pre-compiled versions.

The downloads contain parts of the jbtools library which are distributed with kind permission from Bruno Tatibouet, Université de Franche-Comté, France.

A user manual is available (pdf format).

The installation instructions are here and the release history is here. Don't forget to check the updates. A preliminary FAQ document is available.

ProB Mailing List

We are starting up a mailing list for ProB users. To subscribe to the prob-users mailing list, click on this link this link and send the email. An email is sent back to you, containing an authentication.

Papers

A paper describing the ProB system has been presented at FME'03 in Pisa, September 2003 and is available in the LNCS proceedings (also check here). The BibTeX entry for the paper is as follows: 
@inproceedings{LeuschelButler:FME03,
   author =    {Michael Leuschel and Michael Butler},
   title =     {Pro{B}: A Model Checker for {B}},
   booktitle = {FME 2003: Formal Methods},
   editor =    {Araki, Keijiro and Gnesi, Stefania and Mandrioli, Dino},
   publisher = {Springer-Verlag},
   series =    {LNCS 2805},
   year =      2003,
   pages =     {855-874},
   isbn =      {3-540-40828-2},
}
A brief, 5-page description of ProB can be found here in PDF format. Other papers related to ProB will appear in ZB'2005, FM'2005, and ICFEM'05. A tutorial on ProB will be held at ZB'2005.

Some Screenshots

Screenshots can be found here.

Upcoming Features

We are working on:

Michael Leuschel