Problem Set 4: Modal Logic and Model Checking with NuSMV (due Wed April 13)
The short essay entitled Dekker (available on the private course web site) describes a series of attempts, some flawed, to solve the mutual exclusion problem. Your task in this problem set is to model each of the 4 attempts, to write appropriate specifications in temporal logic, and to analyze them for counterexamples.
You should use the NuSMV model checker, which you can download from the NuSMV website. Make sure you select the version that includes the Chaff SAT solver (so that you can do bounded analyses of LTL specifications). You will also need to download and install the Expat package, which can be downloaded from sourceforge. The Expat download comes with these instructions for installing it. You should install and run NuSMV right away so that we have time to help you if you encounter technical problems.
Running NuSMV is easy. Execute bin/NuSMV and pass it a file containing an SMV machine. This will syntax-check the machine and check any CTL/LTL specs in that file. There is an exellent tutorial available from the website which will show you how to write and check NuSMV models. The NuSMV website also contains a number of examples, but most of them are quite complex; the examples in the tutorial are much more managable. You may find the following two examples written by the TA of some help: trafficlight.smv, trafficlight2.smv. The NuSMV distribution contains the following model about semaphore which will help you to structure your models (but which solves a slightly different algorithm): semaphore.smv.
Your solution should include:
- * 4 models, corresponding to Versions 1 through 4 of the mutual exclusion algorithm in the essay;
- * For each model, a few appropriate temporal logic specifications that illustrate the points made in the text;
- * The results of checking each of the specifications;
- * A brief commentary explaining what you did and what you learned from it. What were the strengths and weaknesses of this style of modeling?
You should make an effort to write specifications in both LTL and CTL, explaining why you choose one formalism over the other.
Please recall the somewhat exacting submission instructions.