No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
{| cellpadding="5" | {| cellpadding="5" | ||
|-valign="top" | |-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. | |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, [[Constraint_Based_Checking|deadlock checking]] and [[Test_Case_Generation|test-case generation]]. | ||
The B language is rooted in predicate logic, arithmetic and set theory and provides support for data structures such as (higher-order) relations, functions and sequences. | |||
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], | 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. | [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]. | 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] or by [http://nobreach.io Nobreach]. | ||
It can be used within [http://www.atelierb.eu/en/2016/02/18/atelier-b-4-3-1-is-available-for-maintenance-holders/|Atelier-B as a disprover and prover]. | It can be used within [http://www.atelierb.eu/en/2016/02/18/atelier-b-4-3-1-is-available-for-maintenance-holders/|Atelier-B as a disprover and prover]. | ||
| Line 31: | Line 32: | ||
== Implementation == | == 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 | 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 [[Using_ProB_with_Z3|an integration with the SMT solver Z3]]. An alternate [[TLC|model checking engine (using TLC)]] well-suited for lower level B specifications is also available. | ||
The [[ProBLicence | ProB Licence can be found here]]. | |||
== Features == | == 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|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 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|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 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 is an animator, constraint solver and model checker for the B-Method (see the 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.
The B language is rooted in predicate logic, arithmetic and set theory and provides support for data structures such as (higher-order) relations, functions and sequences. In addition to the B language, ProB also supports Event-B, CSP-M, TLA+, and Z. ProB can be installed within Rodin, where it comes with BMotionStudio to easily generate domain specific graphical visualizations. ProB is being used within Siemens, Alstom, and several other companies for data validation of complicated properties for safety critical systems. Commercial support is provided by the spin-off company Formal Mind or by Nobreach. It can be used within as a disprover and prover. Part of the research and development was conducted within various research projects, such as the EPSRC funded projects ABCD and iMoc, the EU funded projects Rodin, Deploy and Advance as well as the DFG project Gepavas. Automatically generated test coverage reports are available. |
News
22/4/2016 ProB 1.6.0 is available. Highlights: directed model checking, Z3 available as backend, B line comments and unicode symbols, improved error messages, performance improvements. 19/2/2015 ProB 1.5.0 is available. Highlights: improved random enumeration, static symmetry reduction for deferred set elements, MC/DC coverage analysis for guards and invariants, improved TLC interface, bug fixes and improvements. 3/6/2014 ProB supports Event-B Theories. 30/03/2012 A first version of the online ProB Logic Calculator is available. |
The core of ProB is implemented in 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 constraint solver based on Kodkod (and thus SAT) is also available within ProB, as is an integration with the SMT solver Z3. An alternate model checking engine (using TLC) well-suited for lower level B specifications is also available. The ProB Licence can be found here.
ProB covers a 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. It also 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 graphically visualized. ProB also supports Z specifications (ProB in this context is sometimes called ProZ) as well as TLA+ specifications. We now also have an online ProB Logic Calculator.