| # `SPIN VERIFIER's ROADMAP: BUILDING AND VERIFYING Spin MODELS` The following description provides a basic overview of the verification options that can be used with the Spin model checker. This description assumes that Spin has been installed and that you have a standard C compiler (such as gcc) as well. It also assumes that you are familiar with standard shell command use on a Unix-like system (e.g., Ubuntu Linux, MAC-OS-X, or Cygwin on a Windows-PC). ## `-0-` Verification begins with the specification of a prototype of the system to be studied in the specification language supported by Spin. This language is called ProMeLa (short for Process Meta Language), and the model is called a verification model, or a Spin model. By convention, ProMeLa specification files have a `.pml` file extension. Next you must consider how you can express the critical correctness requirements for your model. You can use assertions, end-state labels, progress-state labels, acceptance-state labels, or LTL properties. But don't worry, in most cases of practical interest you will only need assertions, and less frequently simple LTL properties. ## `-1-` For a quick checkout of the model you have just defined: do a simulation run to catch the simpler mistakes. If no flags are provided, Spin performs a random simulation of the model.
    	$ spin spec.pml		# no options: only print statements produce output
It is often very helpful, especially at this stage in debugging the basic verification model, to add printf statements to the specification to make things more clear. You can add more options to see useful things happening. Without additional flags, only print statements that you use in the model will produce output. If there are none, you may want to use some additional flags.
    	$ spin -p spec.pml	# simulation run, show all execution steps
    	$ spin -c spec.pml	# columnated output for message i/o
You can use the command:
    	$ spin --
to see what other options are available for including additional information in the simulation runs. An important one, in case your model can execute forever, is the ability to set an upper-limit on the number of execution steps performed in a simulation. For instance, to limit the simulation to the first 200 steps:
    	$ spin -u200 -p -l -g -v spec.pml
Check in the output of spin -- what the additional flags that are used here do. When done debugging, you can perform a more thorough check of your model with this command:
    	$ spin -a spec.pml		# thorough check
This step can report syntax errors and impurities that the simulation commands don't catch. For feedback on possible redundancies in your specification, try also:
    	$ spin -A spec.pml		# check for redundancies
And, if you really want to get carried away, you can look at the automata descriptions that Spin generates for you for the verifier's use, by executing:
    	$ spin -search -dump spec.pml
    or just
    	$ spin -search -d spec.pml
If, on the other hand you just want to get a quick basic verification run going, use this command, which will compile and run your verification immediately:
    	$ spin -search spec.pml
And the rest, as they say, is just detail. We will indulge in some of that detail in the next few points. ## `-2-` The biggest decision to make is if the model you created is simple enough to perform a fully exhaustive verification on the machine that you are using. The limits, as always, are CPU-time and RAM memory. The good news is that even if you do not have enough time or memory, Spin can be configured to give you the best possible result within the constraints that you do have. We will first consider how you can setup a standard exhaustive verification run. Exhaustive For an exhaustive verification, you can compile the generated verification code as follows.
    	$ spin -search -O2 spec.pml            # use optimized compilation
It is always smart to use the `-O2` flag to optimize the code: it can often reduce the runtime needed by about 50%. If you know how much physical (not virtual) RAM memory your system has, you can use this to restrict the maximum amount that a verification can take to avoid unpleasant paging behavior, for instance, if you have 256 Megabyte available compile as follows.
    	$ spin -search -O2 -DMEMLIM=256 spec.pml   # set memory bound at 256MB
If the amount of memory you have is not sufficient to complete a verification, consider using one of the compression options that Spin supports. For instance:
    	$ spin -search -O2 -DMEMLIM=256 -collapse spec.pml # use compression
or, for a still more aggressive option, try:
    	$ spin -search -O2 -DMEMLIM=256 -hc spec.pml # use hash-compact compression
If also this is insufficient, and your verification still exceeds the memory bounds, switch to Bitstate verification run (also known as a Supertrace verification). Bitstate For a Bitstate verification run, compile as follows.
    	$ spin -search -O2 -bitstate spec.pml    # use bitstate search
1. This is often used as a method of last resort when a full verication is infeasible because of memory limitations or problem size. It can also be used as a fast prescan of a problem, to get an early and quick indication of the presence or absence of errors. ## `-3-` Up to this point we have ignored what type of property you are trying to verify, or what impact problem size may have on your chances of performing a successful verification. We will address these points now. There are four more decisions you have to make to perform verifications optimally. These four decisions are: Selecting the type of property to be verified (safety or liveness) Selecting the maximum search depth, If you use a Bitstate search: selecting the size of the hash-table Selecting the parameters for a replay of an error, if one is found. We'll now explore each of these decisions in more detail. The first decision is to decide if you want to check the model for Safety properties or for Liveness properties. Safety Examples of safety properties are assertion violations, deadlocks (invalid end-states), etc. To check safety properties only (the most frequently used search mode), you can obtain a fast verifier by adding a `-safety` argument:
       		$ spin -search -safety spec.pml
   plus of course any of the other arguments we discussed earlier, for instance:
       		$ spin -search -O2 -bitstate -safety spec.pml
   In this case you can also use Spin's breadth-first search mode, which works only for safety properties but has the advantage of finding the shortest possible error traces:
       		$ spin -search -bfs spec.pml
   again combined with any other options you need. Liveness Examples of liveness properties are non-progress or acceptance cycles. LTL properties can express both safety and liveness properties. In case of doubt: assume you have a liveness property. To perform a search for violations of general liveness properties you use the runtime parameter `-a` following the `-search` argument to Spin. For instance:
       		$ spin -search -a spec.pml
   plus any other runtime arguments you selected. Non-Progress A non-progress cycle is an infinite execution that never passes through any state in the specification that is marked with a labelname that starts with the prefix "progress". To search for non-progress cycles you add run-time option `-l`, for instance as in:
       		$ spin -search -l spec.pml
2. plus any other runtime arguments you selected. By default the Spin verifiers enforce a search depth restrictionof 10,000 steps. In most cases this will suffice, but when it doesn't the search depth will artificially be truncated to 9,999 steps and become incomplete. You can define a different search-depth by adding a runtime parameter `-m`. For instance:
       	$ spin -search -m100000 spec.pml
   (again, combined with any other options you select). You can also try to set a lower search depth to try to find a shorter variant of an error sequence. For instance
       	$ spin -search -m40 spec.pml
   But in thise case there is no guarantee that if a shorter error sequence exists it will also be found. To get that guarantee you also have to instruct Spin to modify the search algorithm itself, with a runtime parameter `-i` to force a search for a short error. For instance, to search for errors shorter than 100 steps:
       	$ spin -search O2 -i -m100 spec.pml	# iterative search for short errors
4. If you perform a `Bitstate` verification (i.e., you used the search argument `-bitstate`), the size of the memory arena that is used to store states very compactly is determined by your choice of a `-w` parameter. By default, this parameter is set to `-w27`, which defines a memory arena of 227 bits, corresponding to a modest 16 MB of RAM. For maximum coverage you want to set the hash-array size to the maximum size of memory you can grab without making the system page (i.e., below the amount of real physical RAM memory that you can access). More specifically, for maximum coverage, the value you set with the `-w` parameter should at least be larger than the nearest power of 2 of the number of reachable system states that you expect, without exceeding your physical memory size. (And for obvious reasons, you cannot allocate more than about 2 GB of memory on a 32-bit system. For larger memory arenas you will have to use a 64-bit system.) For instance, use `-w23` if you expect less than 8 million reachable states and can use 8 million bits of memory (i.e., 223 bits equals 8 million bits, which equals 220 bytes or 1 MB of RAM). A `-w` value lower than required for full coverage will give you a faster run, but less coverage. A value higher than needed, will give you a slower run, but it will also cover a larger fraction of the statespace. If the verifier finds an error, any error, it will write an error-trail into a file named `spec.pml.trail`, if `spec.pml` is the name of your Spin model. To inspect the trail, and examine the cause of the error, you can use Spin's guided simulation option -replay. For instance:
       	$ spin -p -replay spec.pml
       or
       	$ spin -c -replay spec.pml
   Note that options to spin like `-p` and `-c` go before the `-replay` argument. If, however, a replay must be done with the executable verifier `./pan`, which automatically happens for all models that contain embedded C code fragments in `c_expr` or `c_code` statements, then replay options to the executable verifier are placed after the `-replay` argument, for instance as in: `spin -replay -P2 spec.pml`. The executable verifier accepts different options for replay then spin itself, so it is good to keep these separate. Options placed after the `-replay` argument for a pure Promela model, and options placed before the `-replay` argument for a model with embedded C code, are politely ignored. Add as many extra or different options as you need to pin down the error. (Remember, you can check Spin's available options by executing: `spin --`, and options of the executable verifier with `./pan --`.) One option is to convert the trail into a Tcl/Tk represetation of a message sequence chart of send and receive actions, which will then be displayed with the `wish` command (assuming `wish` is installed on your system):
       	$ spin -M -replay spec.pml
   For more detailed tracebacks you can use, for instance:
       	$ spin -r -s -l -g -replay spec.pml
   Make sure the file `spec.pml` didn't change since you generated the verifier. Spin will warn if you did. If you're not interested in the first error that is reported, add runtime option `-c` to select others:
       	$ spin -search ... -c3 spec.html
   generates a counter-example trail for the third error found in the search. If you just want to count all errors and not see them, use
       	$ spin -search ... -c0 spec.html
   By default, the argument to -c is 1. If you want to obtain a trail for each and every error found (usually not recommended, because there may be an overwhelming number of these), use:
       	$ spin -search ... -c0 -e spec.html
   This creates a series of error trails in files numbers `spec2.pml.trail`, `spec3.pml.trail`, ...etc. To trace back a specific one of these trails, you can specify the specific trail file you want to see with a -k option:
       	$ spin -k trailfilename -p -replay spec.pml
## `Finally` Internally Spin and pan deal with a formalization of the model in terms of automata. Spin assigns numbers to all statements in the input. These state numbers are listed in all output so that you can, if you want, use that information to track down what happens. To see the state assignments use the runtime option -d for the executable verifier pan:
    	$ spin -o3 -search -d spec.pml	# show optimized state machines
to print the optimized state machine assignments, as it is used during verification. (The `-o3` argument turns off a default statement merging option that can sometimes make it harder to interpret the output.) The unoptimized machine (used during random or guided simulations with spin -replay for instance) can also be printed, but you need the executable verifier for that. (It will exist if you've executed the above command first):
    	$ spin -o3 -search -d -d spec.pml	# show full, unoptimized state machines
These two options should also make it easier to understand and verify the working of Spin and `pan` in terms of the underlying automata theoretic foundation. In very rare cases, when you need to debug the working of the verifier itself, you can also consider compiling the verifier with an additional compiler directive `-DCHECK` or `-DVERBOSE`.
Spin HomePage |  | `(Page Updated: 8 June 2014)`