No edit summary |
|||
| Line 6: | Line 6: | ||
[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 now being used within Siemens and | ProB is now being used within Siemens, Alstom, and several other companies for [www.data-validation.fr data validation] of complicated properties. Commercial support is provided by the spin-off company [http://www.formalmind.com Formal Mind]. | ||
Part of the research and development was conducted within 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], and within the EU funded project [http://rodin.cs.ncl.ac.uk/ Rodin]. Development is continued under the EU funded projects [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]. | Part of the research and development was conducted within 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], and within the EU funded project [http://rodin.cs.ncl.ac.uk/ Rodin]. Development is continued under the EU funded projects [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]. | ||
| ProB is an animator and model checker for the B-Method (see the B Site Pages and the B-Method site of Clearsy). It allows fully automatic animation of many B specifications, and can be used to systematically check a specification for 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 B, ProB now 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 now being used within Siemens, Alstom, and several other companies for [www.data-validation.fr data validation] of complicated properties. Commercial support is provided by the spin-off company Formal Mind. Part of the research and development was conducted within the EPSRC funded projects ABCD and iMoc, and within the EU funded project Rodin. Development is continued under the EU funded projects Deploy and Advance as well as the DFG project Gepavas. Automatically generated test coverage reports are available. |
News
4/3/2013 ProB 1.3.6 is available. Highlights: improved constraint propagation for division, modulo, intervals, model checking progress bar, performance improvements, improved Kodkod backend and use within REPL, and many more. 8/10/2012 ProB 1.3.5 is available. Highlights: support for external and recursive functions, optional Kodkod backend, TLA+ support, performance improvements, pragmas, units inference, and many more. 30/03/2012 A first prototype of an online ProB Logic Calculator is available. 21/11/2011 ProB 1.3.4 is available. Highlights: Evaluation View and Eval window, CSP assertion checking, improved editor, 64-bit version for Mac and Linux, performance improvements, and many more. 10/02/2011 ProB 1.3.3 and ProB for Rodin 2.3 is available. Highlights: improved performance, constrained-based deadlock checking, record detection, and many more. 07/30/2010 ProB 1.3.2 is available. Highlights: improved performance, constraint solving over integers (enable in Advanced Preferences), much improved Z support, and many more. 12/07/2009 ProB 1.3.1 is available. Highlights: new data-structure for large sets and relations (see FM 2009), multi-level validation for Event-B, improved constraint propagation for boolean connectives, and many more. 03/20/2009 ProB 1.3.0 is available for download. Highlights: New parser and integrated typechecker, install as AtelierB plugin, improved kernel with support for large sets/relations, improved CSP support, faster LTL model checker, Undo/Redo in text editor, graphical formula viewer, user definable custom animations with gifs. |
The core of ProB is implemented in 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 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). We now also have an online ProB Logic Calculator.