0.5 Using temporal logic to specify properties  (Page 10/11)

Through this section, we've seen some of the common patterns that can arise in the formulas.Following upon the idea of Design Patterns as describing common programming idioms,``Specification Patterns'' describe common logic specification idioms.For a list of LTL specification patterns, see Property Pattern Mappings for LTL .

In addition, there are also algebraic equivalences for LTL,just as there are for propositional logic . We have already seen a DeMorgan-like example; there are also less obvious equivalences, such as distributing $\square ◇$ over $$ : $\square ◇()(\square ◇\square ◇)$ and the redundancy of $\square$ -over- $$ : $(\square \square )\square (\square \square )$ It can be fun to dabble in rewriting LTL formulas, but (alas) we won't visit that topic further here.

Using temporal logic in spin

So, we have a Promela program and an LTL formula to verify. How do we use the tool? In SPIN, in the "Run" menu,select "LTL Property Manager". This opens a new window. The top half contains several subpartsfor entering an LTL formula, while the bottom half is for using it.

In the "Formula" textbox, you can type an LTL formula. If you prefer, you can enter the operators using the buttons below,rather than typing. Also, you can use the "Load" button to restore a previously-saved LTLformula from a file. For a formula, the next checkboxes allow you to either verify thatthe formula always holds or never holds. The "Notes" textbox is simply descriptive text. If you plan on savingthe formula, it is helpful to remind yourself what this formula means and is used for.The "Symbol Definitions" textbox is where the LTL variables (typically p , q , etc. ) are related to the Promela code.This is done through #define s which are temporarily added to your Promela code.

Let's consider another critical section example. The following code simply puts the critical section into a loop. Also included isour standard code to check that the mutual exclusion property is satisfied, although the assertion is commented out. 1 /* Number of copies of the process to run. */ 2 #define NUM_PROCS 33 4 show bool locked = false;5 show int num_crit = 0; 67 active[NUM_PROCS] proctype loop()8 { 9 do10 :: true ->11 12 atomic {13 !locked ->14 locked = true; 15 }16 17 /* Critical section of code. */18 /* Something interesting would go here. */ 1920 num_crit++; 21 /* assert(num_crit == 1); */22 num_crit--; 2324 locked = false; 25 /* End critical section of code. */26 od; 27 }

Using temporal logic, we can accomplish the same check without the assertion.There are several similar ways of doing this.

One way is to verify that num_crit always has the value 0 or 1. To do this, we'll make the following definitionin xspin's ``Symbol Definitions'' textbox: #define p ((num_crit == 0) || (num_crit == 1)) We then want to verify that $p$ always holds, so our formula is []p and mark that we always want this formula to hold.