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 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.

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.