(Created page with "== A small history of ProB == ProB's development started in 2001 with a first alpha release made in October 2003. It filled a gap in the B tooling landscape at the time, sup...") |
|||
| Line 2: | Line 2: | ||
ProB's development started in 2001 with a first alpha release made in October 2003. | ProB's development started in 2001 with a first alpha release made in October 2003. | ||
It filled a gap in the B tooling landscape at the time, supporting the | It filled a gap in the B tooling landscape at the time, supporting the interactive and automatic validation of high-level specifications. | ||
interactive and automatic validation of high-level specifications. | Indeed, following classical B's correct-by-construction approach it is vital that the high-level specifications correctly capture the high-level requirements and functionality. | ||
Indeed, following classical B's correct-by-construction approach it is vital that the high-level specifications correctly capture the high-level requirements | |||
Only the B-Toolkit animator provided some very limited form of validation, and required the user to provide values for parameters and existentially quantified variables, the validity of which was checked by the BToolkit prover. | Only the B-Toolkit animator provided some very limited form of validation, and required the user to provide values for parameters and existentially quantified variables, the validity of which was checked by the BToolkit prover. | ||
ProB's development started in 2001 with a first alpha release made in October 2003. It filled a gap in the B tooling landscape at the time, supporting the interactive and automatic validation of high-level specifications. Indeed, following classical B's correct-by-construction approach it is vital that the high-level specifications correctly capture the high-level requirements and functionality.
Only the B-Toolkit animator provided some very limited form of validation, and required the user to provide values for parameters and existentially quantified variables, the validity of which was checked by the BToolkit prover. This approach was justified by the undecidability of the B language, but was tedious for the user and prevented automated validation. In contrast, ProB allows fully automatic animation of specifications, i.e., values for constants, parameters are computed by ProB's constraint solver rather than explicitly given by users.
Using a variety of explicit-state and symbolic model checking approaches, ProB can be used to systematically check a specification for invariant violations~\cite{DBLP:journals/sttt/LeuschelB08,kringsleuschelsymbolicmc}. Furthermore, ProB supports LTL model checking using a tableau-based algorithm as outlined in~\cite{Plagge:2010:SOS:1714440.1714445,10.1007/978-3-319-41591-8_14}. Distributed explicit state model checking is supported via a C extension~\cite{distb} and by using an integration with the language-independent model checker \textsc{LTSmin}~\cite{ltsminintegration}.
Both model checking and animation are driven by a backend written in SICStus Prolog~\cite{carlsson2012sicstus}, implementing a solver for set-theory and predicate logic using Prolog co-routines and attributed variables along with the finite domain constraint logic programming library~\cite{sicstusclpfd} of SICStus Prolog.
Unknown to the ProB team at the time (around 2000), another team pursued similar ideas leading to the CLP-S solver \cite{Bouquet:TACAS02} and the BZTT tool \cite{Ambert:FATES02} based on it. This work also gave rise to a company (Lerios), which concentrated on model-based test-case generation and later ported the technology to an imperative programming language. Unfortunately, the development of BZTT and CLP-S has been halted; the tool is no longer available.
Model checking aside, the constraint-solving capabilities of ProB can also be used for model finding, deadlock checking as well as test-case generation and drive many of the animation, visualisation and data validation tools that will be discussed below.