No edit summary |
|||
| Line 32: | Line 32: | ||
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 available as is an integration with [https://github.com/utwente-fmt/ltsmin/releases LTSmin] as [[LTSmin|model checking backend]]. | 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 available as is an integration with [https://github.com/utwente-fmt/ltsmin/releases LTSmin] as [[LTSmin|model checking backend]]. | ||
The [[ProBLicence | ProB Licence can be found here]]. | The [[ProBLicence | ProB Licence can be found here]]. | ||
|
ProB is an animator, constraint solver and model checker for the B-Method. The constraint-solving capabilities of ProB can be used for animation, model finding, constraint-based symbolic 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. ProB can also be used as a Jupyter kernel to generate interactive notebooks. ProB is being used within Alstom, ClearSy, Siemens, Thales and several other companies for data validation of complicated properties for safety critical systems. It was used, e.g., for Paris Line1, Sao Paulo line 4, Barcelona line 9 and many more. ProB is certified T2 SIL4 according to the Cenelec EN 50128 standard for use at Thales. In this video from the Deutsche Bahn you can see ProB animating a formal B model of the ETCS hybrid-level 3 principles in real-time, controlling two trains. Michael Leuschel and his group have won the first edition of the AlainColmerauer Prize for ProB. For commercial support contact Michael Leuschel.
Versions of ProBSeveral versions of ProB are available. They all make use of the same Prolog core (see below).
ImplementationThe 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 available as is an integration with LTSmin as model checking backend. The ProB Licence can be found here.
|
News
4/4/2023 ProB 1.12.0 is available. Call stack infos, performance improvements in parser and solver, new LTL operators, VISB improvements, reals/floats for Rodin theories. 10/11/2022 Michael Leuschel and his group win first edition of Colmerauer Prize for ProB 29/12/2021 ProB 1.11.1 is available. Identifiers between backquotes, flexible JSON trace replay, DPLLT solving, improvements to Z3 backend. 6/10/2021 ProB 1.11.0 is available. Improved support for infinite sets, operation caching, faster LTL checking for safety formulas, more compact .prob files, VisB HTML export, constructive Z3 translation. 26/1/2021 ProB2-UI 1.1.0 is available, contains VisB. 15/12/2020 ProB 1.10.0. Highlights: well-definedness prover, REAL datatype, -lint comand for VSCode and Atom, improved unsat core. 19/2/2020 ProB 1.9.3. Highlights: performance improvements, new external functions, performance monitoring, notarized for macOS. 12/7/2019 ProB 1.9.0. Highlights: Unicode support, regular expression library, memoization. New ProB2 UI. 1/10/2018 ProB 1.8.2. Highlights: Jupyter kernel, first support for Alloy models. 11/7/2017 ProB 1.7.0 Highlights: improved Latex document generation, improved XML/CSV support, RULE DSL language. 20/10/2016 ProB 1.6.1 Highlights: LET and IF-THEN-ELSE for expressions and predicates. 22/4/2016 ProB 1.6.0 highlights: directed model checking, Z3 as backend. 18/8/2014 ProB 1.4.0 is available. Highlights: CLP(FD)-based constraint solver enabled by default, integration of the TLC model checker. 4/3/2013 ProB 1.3.6 is available. Highlights: model checking progress bar, improved Kodkod backend and use within REPL. 30/03/2012 ProB Logic Calculator available. |
ProB covers a large part of B, and we are striving towards full coverage of Atelier B constructs. ProB supports B features such as non-deterministic operations, arbitrary quantification, sets, sequences, functions, lambda abstractions, set comprehensions, records, and many more. ProB does support multiple machines, refinements, and implementations. ProB can also be used for automated refinement checking and LTL model checking. It also supports CSP-M process descriptions, 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 supports Z specifications (ProB in this context is sometimes called ProZ) as well as TLA+ specifications. ProB can be used within Rodin and Atelier-B as a disprover and prover.
The initial conference publication was:
A later journal article describes ProB in more detail:
For convenience we also provide Bibtex entries for the above references.