Verification

Verification option in the Menu Bar Run command 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 on 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 is 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.