D45 Model Checking

Overview

TODO An overview of the work done about model checking.

State Space Reduction, Compression and Hashing

Driven by a case study from the space sector (a protocol modeled by SSF), where memory consumption was an issue, we have investigated ways to reduce ProB's memory consumption. A first step was to implement a first version of state compression, whereby we simplify stored states so that they require less memory. This was achieved without compromising speed and is now always activated. Furthermore, if the preference COMPRESSION is set to true, then ProB will also detect common (sub-)expressions in states and store the common expressions only once. E.g., when several states have the same same value for a given variable x then its value will only be stored just once. This is particularly useful when complicated variables only change infrequently.

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 (common subexpressions are detected by hashing). We have also implemented a cryptographic SHA1 hashing function for Prolog terms, but it is not yet used in the production version of ProB.

Finally, the most useful symmetry reduction technique of ProB is the so-called "hash marker" method. Here, we have also improved the computation of the hash symmetry markers, both achieving a reduction in size and runtime.

Constraint-Based Checking

Improved Constraint-based checking for deadlocks, invariants and event sequences (used in MBT). In addition, many improvements in constraint solving kernel were implemented.

Experiments

Conducted comparison with TLA+ model checker TLC

Motivations

TODO To be completed. The motivations for the state space compression arose from experiments in WP3 (space), and from applications of ProB outside of Deploy.

The need for constraint-based deadlock checking arose in the automotive work package, more precisely during the elaboration of the cruise control system. Here, proving turned out to be impractical and ProB was used to find deadlocks and guide the development of the model.

Choices / Decisions

TODO To be completed.

Aggressive compression can also induce a performance penalty. The new default mode was chosen such that there should be no performance penalty, with reduced memory usage. (Indeed, the time for compression is regained by reduced time to store and retrieve the states.)

A more aggressive setting can be forced by -p COMPRESSION TRUE. This will further reduce memory consumption, but may increase runtime (although quite often it does not).

Available Documentation

TODO To be completed.

• Command-Line Version of ProB
• Constraint-Based Deadlock Checking of High-Level Specifications. In Proceedings ICLP'2011 (to appear), Cambridge University Press, 2011.
• Translating TLA+ to B and experiments with TLC

Status

TODO To be completed.

The improved hashing and light-weight state compression is available in the current release of ProB. The SHA1 hash technique is not available in the current release. The research on further compression technique is ongoing and will be continued within the project ADVANCE.