The ProB Animator and Model Checker: Difference between revisions

Latest revision as of 14:53, 7 March 2024

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 ProB

Several versions of ProB are available. They all make use of the same Prolog core (see below).

A command-line tool called probcli. It is distributed with the standard download of the latest release.
The original graphical user interface ProB Tcl/Tk. It is distributed with the standard download of the latest release.
The new graphical user interface ProB2-UI based on Java FX and the ProB2-Java-API of ProB. It is available as a separate download. It contains VisB for SVG-based visualizations (as a successor to BMotionStudio).
ProB for use within Rodin, the toolset for Event-B. It is available as a plugin.
An API for using ProB from Java, called ProB2-Java-API (aka ProB2). It is available via Maven Central.
A kernel for Jupyter, allowing to use B and ProB from within Jupyter notebooks. It is available via a seperate installation procedure.

Implementation

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 available as is an integration with LTSmin as model checking backend. The ProB Licence can be found here.

News

2024-02-20 ProB 1.13.0 is available. Better Rodin theory support. Template strings. READ_JSON and other new external functions. VisB support for groups and "use" element. MCTS game play.

2023-08-10 ProB 1.12.2 is available. VisB improvements.

2023-04-04 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.

2022-11-10 Michael Leuschel and his group win first edition of Colmerauer Prize for ProB

2021-12-29 ProB 1.11.1 is available. Identifiers between backquotes, flexible JSON trace replay, DPLLT solving, improvements to Z3 backend.

2021-10-06 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.

2021-01-26 ProB2-UI 1.1.0 is available, contains VisB.

2020-12-15 ProB 1.10.0. Highlights: well-definedness prover, REAL datatype, -lint comand for VSCode and Atom, improved unsat core.

2020-02-19 ProB 1.9.3. Highlights: performance improvements, new external functions, performance monitoring.

2019-07-12 ProB 1.9.0. Highlights: Unicode support, regular expression library, memoization. New ProB2 UI.

2018-10-01 ProB 1.8.2. Highlights: Jupyter kernel, first support for Alloy models.

2017-07-11 ProB 1.7.0 Highlights: improved Latex document generation, improved XML/CSV support.

2016-10-20 ProB 1.6.1 Highlights: LET and IF-THEN-ELSE for expressions and predicates.

2016-04-22 ProB 1.6.0 highlights: directed model checking, Z3 as backend.

2014-08-18 ProB 1.4.0 is available. Highlights: CLP(FD)-based constraint solver enabled by default, integration of the TLC model checker.

2012-03-30 ProB Logic Calculator available.

Features

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.

Citing ProB

The initial conference publication was:

Michael Leuschel & Michael Butler (2003): ProB: A Model Checker for B. In Keijiro Araki, Stefania Gnesi & Dino Mandrioli, editors: FME 2003: Formal Methods, LNCS 2805, Springer-Verlag, pp. 855–874, doi:10.1007/978-3-540-45236-2 46.

A later journal article describes ProB in more detail:

Michael Leuschel & Michael J. Butler (2008): ProB: an automated analysis toolset for the B method. STTT 10(2), pp. 185–203. Available at http://dx.doi.org/10.1007/s10009-007-0063-9.

For convenience we also provide Bibtex entries for the above references.

@@ Line 1: / Line 1: @@
 {| cellpadding="5"
 |-valign="top"
-|width="60%"|ProB is an animator and model checker for the [http://en.wikipedia.org/wiki/B-Method B-Method] (see the [http://www-lsr.imag.fr/B/Bsite-pages.html B Site Pages] and the [http://www.bmethod.com/ 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.
+|width="60%" style="padding-right:20px;" |
+ProB is an animator, constraint solver and model checker for the [http://www.clearsy.com/en/our-specific-know-how/b-method/?lang=en B-Method]. The constraint-solving capabilities of ProB can be used for animation, model finding, [[Constraint_Based_Checking|constraint-based symbolic checking]] and [[Test_Case_Generation|test-case generation]].
-In addition to B, ProB now also supports [http://www.event-b.org/ Event-B], [http://en.wikipedia.org/wiki/Communicating_sequential_processes CSP-M],
+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.
-[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.
+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].
+ProB can also be used as a [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel Jupyter kernel] to generate interactive notebooks.
-ProB is now being used within Siemens, Alstom, and several other companies for [http://www.data-validation.fr data validation] of complicated properties. Commercial support is provided by the spin-off company [http://www.formalmind.com Formal Mind].
+ProB is being used within Alstom, ClearSy, Siemens, Thales and several other companies for [http://www.data-validation.fr 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 [https://www.youtube.com/watch?v=K6mS6akRmvA 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 <b>[https://prologyear.logicprogramming.org/ColmerauerPrize.html  AlainColmerauer Prize]</b> for ProB.
+For commercial support contact [http://www.stups.uni-duesseldorf.de/~leuschel/ Michael Leuschel].
-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].
-Automatically generated test [http://nightly.cobra.cs.uni-duesseldorf.de/coverage/html/ coverage reports are available].
+=== Versions of ProB ===
-|width="40%" style="background:#EDF2F2;" | '''News'''
+Several versions of ProB are available. They all make use of the same Prolog core (see below).
-'''4/3/2013'''
-[[Download|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'''
+* A command-line tool called [[Using_the_Command-Line_Version_of_ProB|probcli]]. It is distributed with the standard [[Download#Latest_Release|download of the latest release]].
-[[Download|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.
+* The original graphical user interface ProB Tcl/Tk.  It is distributed with the standard [[Download#Latest_Release|download of the latest release]].
+* The [[ProB2-UI|new graphical user interface ProB2-UI]] based on Java FX and the ProB2-Java-API of ProB. It is available as a  [[Download#ProB2_UI_using_Java_FX| separate download]]. It contains [[VisB]] for SVG-based visualizations (as a successor to BMotionStudio).
+* [[ProB_for_Event-B|ProB for use within Rodin]], the toolset for Event-B. It is [[Download#ProB_for_Rodin|available as a plugin]].
+* An API for using ProB from Java, called [[ProB_Java_API|ProB2-Java-API]] (aka ProB2). It is available via [https://search.maven.org/search?q=a:de.prob2.kernel Maven Central].
+* A [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel kernel for Jupyter], allowing to use B and ProB from within Jupyter notebooks. It is available via [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel a seperate installation procedure].
-'''30/03/2012'''
-A first prototype of an online [[ProB_Logic_Calculator|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'''
+=== Implementation ===
-ProB 1.3.3 and ProB for Rodin 2.3 is available. Highlights: improved performance, constrained-based deadlock checking, record detection, and many more.
+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]].
-'''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'''
+|width="40%" style="background:#EDF2F2;padding:15px;" | '''News'''
-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.
+'''2024-02-20'''
+[[Download|ProB 1.13.0]] is available. Better Rodin theory support. Template strings.  READ_JSON and other new external functions. VisB support for groups and "use" element. [[Monte_Carlo_Tree_Search_Game_Play|MCTS game play]].
-'''03/20/2009'''
+'''2023-08-10'''
-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.
+[[Download|ProB 1.12.2]] is available. [[VisB#VisB_DEFINITIONS_2 |VisB]] improvements.
+'''2023-04-04'''
+[[Download|ProB 1.12.0]] is available. Call stack infos, performance improvements in parser and solver,  new [[LTL_Model_Checking#Supported_Syntax |LTL]] operators, [[VisB#VisB_Additional_SVG_Objects|VisB]] improvements, reals/floats for [[Event-B_Theories|Rodin theories]].
+'''2022-11-10'''
+Michael Leuschel and his group win [https://prologyear.logicprogramming.org/ColmerauerPrize.html  first edition of Colmerauer Prize] for ProB
+'''2021-12-29'''
+[[Download|ProB 1.11.1]] is available. Identifiers between backquotes, flexible JSON trace replay, DPLLT solving, improvements to Z3 backend.
+'''2021-10-06'''
+[[Download|ProB 1.11.0]] is available. Improved support for infinite sets, operation caching, faster LTL checking for safety formulas, more compact .prob files, [[VisB|VisB]] HTML export, constructive Z3 translation.
+'''2021-01-26'''
+[[Download#ProB2-UI_using_Java_FX|ProB2-UI 1.1.0]] is available, contains [[VisB|VisB]].
+'''2020-12-15'''
+[[Download|ProB 1.10.0]]. Highlights: [[Well-Definedness_Checking|well-definedness prover]], [[Summary_of_B_Syntax#Reals:|REAL datatype]], -lint comand for [[Editors_for_ProB#VSCode|VSCode]] and [[Editors_for_ProB#Atom|Atom]], improved unsat core.
+'''2020-02-19'''
+[[Download|ProB 1.9.3]]. Highlights: performance improvements, new external functions, performance monitoring.
+'''2019-07-12'''
+[[Download|ProB 1.9.0]]. Highlights: Unicode support, regular expression library, memoization. [[Download#ProB2_UI_using_Java_FX|New ProB2 UI]].
+'''2018-10-01'''
+[[Download|ProB 1.8.2]]. Highlights: [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel Jupyter kernel], first [[Alloy|support for Alloy models]].
+'''2017-07-11'''
+[[Download|ProB 1.7.0]] Highlights: improved [[Generating_Documents_with_ProB_and_Latex |Latex document generation]], improved XML/CSV support.
+'''2016-10-20'''
+[[Download|ProB 1.6.1]] Highlights:  [[Tips:_B_Idioms |LET and IF-THEN-ELSE for expressions and predicates]].
+'''2016-04-22'''
+[[Download|ProB 1.6.0]] highlights: [[Tutorial_Directed_Model_Checking|directed model checking]], [[Using_ProB_with_Z3|Z3 as backend]].
+'''2014-08-18'''
+[[DownloadPriorVersions |ProB 1.4.0]] is available. Highlights: CLP(FD)-based constraint solver enabled by default, [[TLC|integration of the TLC model checker]].
+'''2012-03-30''' [[ProB_Logic_Calculator|ProB Logic Calculator]] available.
+''' '''
+[[Download#Short Release History|More in Release History]]
 |}
-== Implementation ==
+=== Features ===
-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). It uses co-routining and finite domain constraint solving to make animation of B machines possible. The [[ProBLicence | ProB Licence can be found here]].
+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 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 supports Z specifications (ProB in this context is sometimes called [[ProZ]]) as well as [[TLA|TLA+ specifications]].
+ProB can be used within Rodin and [http://www.atelierb.eu/en/ Atelier-B as a disprover and prover].
+[[File:ProBAtAGlance.png| center |500px]]
+=== Citing ProB ===
+The initial conference publication was:
+* Michael Leuschel & Michael Butler (2003): ProB: A Model Checker for B. In Keijiro Araki, Stefania Gnesi & Dino Mandrioli, editors: FME 2003: Formal Methods, LNCS 2805, Springer-Verlag, pp. 855–874, doi:10.1007/978-3-540-45236-2 46.
+A later journal article describes ProB in more detail:
+* Michael Leuschel & Michael J. Butler (2008): ProB: an automated analysis toolset for the B method. STTT 10(2), pp. 185–203. Available at [http://dx.doi.org/10.1007/s10009-007-0063-9 http://dx.doi.org/10.1007/s10009-007-0063-9].
+For convenience we also provide  [[Citing ProB|Bibtex entries for the above references]].
-== Features ==
+__NOTOC__
-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]]). We now also have an online [[ProB Logic Calculator]].