The ProB Animator and Model Checker

2015-10-15T11:16:59Z

134.99.112.66: /* Implementation */

{| cellpadding="5"
|-valign="top"
|width="60%" style="padding-right:20px;" |ProB is an animator, constraint solver and model checker for the [http://en.wikipedia.org/wiki/B-Method B-Method] (see the [http://www.clearsy.com/en/our-specific-know-how/b-method/?lang=en B-Method site of Clearsy]). It allows fully automatic animation of B specifications, and can be used to systematically check a specification for a wide range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation.

In addition to the B language, ProB also supports [http://www.event-b.org/ Event-B], [http://en.wikipedia.org/wiki/Communicating_sequential_processes CSP-M],
[http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+], and [http://en.wikipedia.org/wiki/Z_notation Z]. ProB can be installed within [http://sourceforge.net/projects/rodin-b-sharp/ Rodin], where it comes with [http://www.stups.uni-duesseldorf.de/BMotionStudio/ BMotionStudio] to easily generate domain specific graphical visualizations.

ProB is being used within Siemens, Alstom, and several other companies for [http://www.data-validation.fr data validation] of complicated properties for safety critical systems. Commercial support is provided by the spin-off company [http://www.formalmind.com Formal Mind].

Part of the research and development was conducted within various research projects, such as the [http://www.epsrc.ac.uk/default.htm EPSRC] funded projects [http://users.ecs.soton.ac.uk/phh/abcd/ ABCD] and [http://users.ecs.soton.ac.uk/mal/ISM.html iMoc], the EU funded projects [http://rodin.cs.ncl.ac.uk/ Rodin], [http://www.deploy-project.eu/ Deploy] and [http://www.advance-ict.eu/ Advance] as well as the [http://www.dfg.de/ DFG] project [http://www.gepavas.de/ Gepavas].

Automatically generated test [http://nightly.cobra.cs.uni-duesseldorf.de/coverage/html/ coverage reports are available].

|width="40%" style="background:#EDF2F2;padding:15px;" | '''News'''
'''19/2/2015'''
[[Download|ProB 1.5.0]] is available. Highlights: improved random enumeration, MACE/SEM style static symmetry reduction for deferred set elements, MC/DC coverage analysis for guards and invariants, improved TLC interface, bug fixes and improvements including but not limited to the constraint solver.

'''3/6/2014'''
ProB supports [[Event-B Theories]].

'''30/03/2012'''
A first version of the online [[ProB_Logic_Calculator|ProB Logic Calculator]] is available.

''' '''
[[Download#Short Release History|More in Release History]]
|}

== Implementation ==
The core of ProB is implemented in [http://www.sics.se/isl/sicstuswww/site/index.html SICStus Prolog] (but can be run without a SICStus Prolog license). The ProB constraint solver is implemented using co-routining and the CLP(FD) finite domain library of SICStus. An alternate [[Using_ProB_with_KODKOD | constraint solver based on Kodkod (and thus SAT)]] is also available within ProB, as is an alternate [[TLC|model checking engine (TLC)]] for low-level B specifications. The [[ProBLicence | ProB Licence can be found here]].x

== Features ==
ProB covers a [[Summary of B Syntax|large part of B]], and we are striving towards full coverage of Atelier B and B4Free constructs. ProB supports B features such as non-deterministic operations, ANY statements, operations with complex arguments, sets, sequences, functions, lambda abstractions, set comprehensions, records, constants and properties, and many more. Not supported are the Atelier B tree operations and there are restrictions on DEFINITIONS. ProB does support multiple machines, refinements, and implementations. ProB can also be used for automated refinement checking and [[LTL Model Checking|LTL model checking]]. It also [[CSP-M|supports almost full CSP-M]] process descriptions (as of version 1.2.7), to be used on their own or to guide B machines for specification and property validation. The state space of the specifications can be [[Graphical Viewer|graphically visualized]].
ProB also supports Z specifications (ProB in this context is sometimes called [[ProZ]]) as well as [[TLA|TLA+ specifications]]. We now also have an online [[ProB Logic Calculator]].

ProB Documentation - User contributions [en]

The ProB Animator and Model Checker