Difference between revisions of "D45 Model Checking"
imported>Leuschel |
imported>Leuschel |
||
| Line 1: | Line 1: | ||
= Overview = | = Overview = | ||
{{TODO}} An overview of the work done about model checking. | {{TODO}} An overview of the work done about model checking. | ||
| + | |||
| + | == State Space Reduction, Compression and Hashing == | ||
Driven by SSF usage of ProB: state compression: simplify states stored so that they require less memory. This was achieved without compromising speed. | Driven by SSF usage of ProB: state compression: simplify states stored so that they require less memory. This was achieved without compromising speed. | ||
| Line 9: | Line 11: | ||
We have also implemented a SHA1 hashing function for Prolog terms, but it is not yet used in the production version of ProB. | We have also implemented a SHA1 hashing function for Prolog terms, but it is not yet used in the production version of ProB. | ||
| + | improved performance for hash symmetry markers: both reduction in size and runtime. | ||
| + | |||
| + | In addition, many improvements in constraint solving kernel. | ||
| + | |||
| + | |||
| + | == Constraint-Based Checking == | ||
| + | |||
| + | Improved Constraint-based checking for deadlocks, invariants and event sequences (used in MBT). | ||
| + | |||
| + | |||
| + | == New Features == | ||
| + | Experiments with Theory Plugin | ||
| + | |||
| + | Support of finite operator | ||
| + | |||
| + | Improved detection of infinite functions, and improved support for them | ||
| + | |||
| + | Detection when infinite sets had to be approximated | ||
| + | |||
| + | |||
| + | |||
| + | == Experiments == | ||
| + | Conducted comparison with TLA+ model checker TLC | ||
= Motivations = | = Motivations = | ||
Revision as of 15:19, 10 February 2012
Contents
Overview
TODO An overview of the work done about model checking.
State Space Reduction, Compression and Hashing
Driven by SSF usage of ProB: state compression: simplify states stored so that they require less memory. This was achieved without compromising speed. If the preference COMPRESSION is set to true, then ProB will also detect common (sub-)expressions and store them only once. E.g., when several states have the same same value for a given variable x then its value will only be stored once.
Related to this aspect, the hashing of ProB states was improved on 64-bit architectures, which is also important in the context of detecting common subexpressions for sharing. We have also implemented a SHA1 hashing function for Prolog terms, but it is not yet used in the production version of ProB.
improved performance for hash symmetry markers: both reduction in size and runtime.
In addition, many improvements in constraint solving kernel.
Constraint-Based Checking
Improved Constraint-based checking for deadlocks, invariants and event sequences (used in MBT).
New Features
Experiments with Theory Plugin
Support of finite operator
Improved detection of infinite functions, and improved support for them
Detection when infinite sets had to be approximated
Experiments
Conducted comparison with TLA+ model checker TLC
Motivations
TODO To be completed.
Choices / Decisions
TODO To be completed.
Available Documentation
TODO To be completed.
Status
TODO To be completed.
