Department of Computer Science
CPSC 513: Intro to Formal Verification and Analysis


Please email me your completed SMV program, including your specifications and fairness constraints, as well as an intuitive description of any bugs you found.

I hope this is an easy and fun exposure to the NuSMV model checker, and CTL model checking in general. NuSMV is a fairly recent re-creation and extension of SMV, which was the original symbolic model checker. There's no an even newer NuXMV, so NuSMV appears to be no longer actively maintained, but it's open-source and NuXMV isn't. (However, you might consider using NuXMV for your project instead of NuSMV, as it's free for non-commercial use.)

Mutual exclusion is a classic problem from concurrent programming, operating systems, distributed systems, etc. The basic problem is to write code for two programs that execute at the same time, and you don't want both of them to execute a special part of the code (called the "critical section") at the same time. In practice, the critical section would be the code required to access a shared resource (shared variable, data file, printer, etc.).

One correct solution (based on Leslie Lamport's Bakery Algorithm) is as follows:


-- Global variables:  n1, n2, both initialized to 0.
-- Process P1
--	1: n1 = 1
--	2: n1 = n2+1;
--	3: if (n2!=0)&(n2<n1) goto 3	-- waiting for critical section
--	4: /* this line is the critical section */
--	5: n1 = 0
--	6: goto 1
-- Process P2
--	1: n2 = 1
--	2: n2 = n1+1;
--	3: if (n1!=0)&(n1<n2) goto 3	-- waiting for critical section
--	4: /* this line is the critical section */
--	5: n2 = 0
--	6: goto 1
Each statement gets executed atomically (in one step), but you can make no assumptions about which process gets to execute at any given moment in time. One problem with this solution is that the global variables can be arbitrarily large integers, which is not implementable in practice. In an attempt to get around this problem, I've inserted an extra loop between statements 1 and 2, which waits in case the global variables get too large. Your job is to use SMV to determine if my attempted fix was successful or not. (Hint: It's not!)

My SMV description of this protocol contains additional details about exactly what properties a correct solution must obey, and what assumptions you can make about the process scheduling. You will need to add CTL (or LTL) specifications to tell SMV what properties you want to check, as well as fairness constraints to eliminate vacuous error traces (e.g. P1 never gets to the critical section because it never gets to execute at all).

For the assignment, you'll need to get the NuSMV model checker. You can download and build it yourself. However, I'm finding that the newest version that used to build easily on our department Linux machines isn't building correctly anymore (apparently problems between Python 2 and 3). Fortunately, they also have pre-compiled binaries for Linux, Windows, and MacOS, so you all should be in good shape. Or on the CS department Linux machines, I put the pre-compiled binary in /isd/users/software/NuSMV-2.6.0-Linux/bin/NuSMV

You'll also definitely need to browse the NuSMV manual.