Verification
Verification option in the Tool Bar opens the quite complex
Verification
preference page. After selecting and/or entering the appropriate
verification parameters and clicking the OK button, the model
syntax check using the default
and extra verifier generation options (if specified on the Verification
preference page) is performed first.
If there is no syntax error within the model, the model-specific verifier
pan.c
source C file is
generated. After that, the C compiler is invoked that compiles the
verifier source file using the compile-time options (according to the
selections in the Verification preference page) to the verifier
executable file called
pan
. Finally, the verifier
runs using the selected options and parameters entered on the Verification
preference page.
From Spin Version 6.4.0 on, the iterative sequential runs or parallel swarm
runs of pan
can be selected in the bitstate hashing storage mode.
In this case, the verifier generation, compilation, and sequential/parallel
runs of pan
are achieved by using spin run-time option
-biterate
or -swarmN,M
. All other verifier generation
options, compile-time directives, and run-time options, specified anywhere on
the Verification preference page, are also considered.
A printout of a verification run is shown in the
Console View.
If the verification finds an error, a counterexample is generated
and saved in a so-called error-trail file with the file extension
.trail
appended to the
original Promela model file name. If selected, multiple error-trail
files may be produced. The trail file(s) can be used in a guided
simulation that replays the execution that violated the property.