Verification preference page

The most complex preference page in SpinRCP is the Verification preference page. In the upper part a user can export current verification parameters (verification profile) to an xml file and import or reload a previously saved verification profile. The current verification profile file name including date and time of its creation are shown. Verification options are accessible below in three tabs: Basic Options, Advanced Options, and Iterative/Swarm Run.

In the Basic Options tab a user can select first a correctness property to be proved (either safety (default) or liveness) and several additional options (assertion violations and invalid end states for safety properties, non-progress or acceptance cycles with/without weak fairness for liveness properties, and whether to report unreachable code and check xr/xs assertions or not for both correctness properties types.

Then, the storage mode (exhaustive, bitstate hashing or hash-compact) can be selected. Two lossless compression methods (minimized automata and collapse compression) are available for the exhaustive storage mode.

If any never claim exists, it may be considered in the model verification process by clicking the Apply never claim button. A never claim can be specified in four different ways. By checking the Use these parameters checkbox, the Compile-time and Run-time text fields become enabled and a user can explicitly enter the compile-time and run-time parameters that supersede the clicked options and parameters entered elsewhere. All other buttons, checkboxes, labels, and text boxes become disabled.

In the Advanced Options tab it is possible to enter several advanced verification parameters (the amount of the available physical memory in megabytes, the estimated state space size, the maximum search depth, number of hash-functions in bitstate mode, the size for minimized automaton, extra verifier generation options, extra compile-time directives, and extra run-time options).

Next, some error-trapping options can be selected. A user can enter an error number at which verification will stop or require that verification does not stop at errors. Additional options in error trapping is to save all error trails, add complexity profiling and compute variable ranges.

Similar as in simulation, the behavior of a full queue in the verification process can be selected. It may either block (default) or lose new messages.

In the last group of options on this tag, two different search modes can be selected (depth-first search (default) or breadth-first search). In both options, partial ordered reduction may be applied for reducing the number of reachable states. In the depth-first search mode, two additional options are available: iterative search for short trail and bounded context switching using a given bound (default 0).

The Iterative/Swarm Run tag can be used to apply iterative sequential or swarm parallel runs of a pan verifier if the bitstate hashing storage mode is selected. If the verification process uses other storage modes, exhaustive or hash-compact, all buttons, labels, and text fields on this tag are disabled.

Two bitstate search refinements are available: iterative sequential runs (default) of pan verifier with the hashtable size increasing step by step from -w18 upto -w35 until an error is found and so-called swarm parallel runs, where N instances of pan verifiers are executed in parallel (on N cores) and -w is incremented every M runs. For each run, several other parameters are also randomized for spreading search in different directions and thus increasing the covered fraction of state space. Values for parameters N and M have to be set. The default value for N and M are 10 and 1, respectively.

A click on the Restore Defaults button restores the default selections of options and default values of parameters.

A click on the Apply button applies the selected options and entered/selected parameters.

A click on the OK button applies the selected options and entered/selected parameters and closes the page. If the Verification preference page is opened after selecting the Verification option in the Menu Bar Run command or in the Tool Bar, a click on the OK button starts the verification.

A click on the Cancel button cancels the selected options and entered/selected parameters, reverts their value to the previous ones and closes the page.