No edit summary |
No edit summary |
||
| Line 15: | Line 15: | ||
== Versions of ProB == | === Versions of ProB === | ||
Several versions of ProB are available. They all make use of the same Prolog core (see below). | Several versions of ProB are available. They all make use of the same Prolog core (see below). | ||
| Line 58: | Line 58: | ||
|} | |} | ||
== 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 [[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. An integration with [https://github.com/utwente-fmt/ltsmin/releases LTSmin] is also available. | 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. An integration with [https://github.com/utwente-fmt/ltsmin/releases LTSmin] is also available. | ||
The [[ProBLicence | ProB Licence can be found here]]. | The [[ProBLicence | ProB Licence can be found here]]. | ||
Automatically generated test [https://www3.hhu.de/stups/internal/coverage/html/ coverage reports are also available]. | Automatically generated test [https://www3.hhu.de/stups/internal/coverage/html/ coverage reports are also available]. | ||
== Features == | === Features === | ||
ProB covers a [[Summary of B Syntax|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|refinement checking]] and [[LTL Model Checking|LTL model checking]]. It also [[CSP-M|supports almost full 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 [[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 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|refinement checking]] and [[LTL Model Checking|LTL model checking]]. It also [[CSP-M|supports almost full 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 [[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 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]. | ProB 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]. | ||
|
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. ProB can now also be used as a Jupyter kernel to generate interactive notebooks. ProB is being used within Siemens, Alstom, Thales and several other companies for data validation of complicated properties for safety critical systems. 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. For commercial support contact the spin-off company Formal Mind or Michael Leuschel.
Versions of ProBSeveral versions of ProB are available. They all make use of the same Prolog core (see below).
|
News
12/7/2019 ProB 1.9.0 is available. Highlights: improved error feedback and Unicode support, regular expression library, memoization. New ProB2 UI. 1/10/2018 ProB 1.8.2 is available. Highlights: Jupyter kernel, first support for Alloy models. 20/03/2018 ProB 1.8.0 is available. Highlights: terminal colours, performance. 5/10/2017 ProB 1.7.1 highlights: performance, Z support, export history to HTML. 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, B line comments and unicode symbols. 19/2/2015 ProB 1.5.0 is available. MC/DC coverage, improved TLC interface. 30/03/2012 ProB Logic Calculator 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. An integration with LTSmin is also available. The ProB Licence can be found here. Automatically generated test coverage reports are also 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 almost full 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 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. ProB can be used within Atelier-B as a disprover and prover.