University of Washington
Spring 2004
instructor: Rob DeLine
ta: Miryung Kim
due Mon 10 May 2004
This assignment will give you the opportunity to practice using model checkers to model and verify distributed systems. You are to work alone on this assignment. You may ask your classmates for clarifications about the assignment, but not discuss solutions. You should feel free to consult the course readings, the lecture notes, and general material from the library or internet that describes model checking and Spin. You should not consult the library or internet for solutions to these assignment questions or similar questions, since that would rob you of the opportunity to hone your abstraction skills. Finally, please monitor the course mailing list for questions and clarifications about the assignment.
In lecture we wrote naive Promela models of an elevator and discussed safety and liveness properties that we can have Spin demonstrate of these models. (One such model and set of LTL formulae are posted on the course web site.) This problem is to extend the model to be less naive and to give you practice using Promela and Spin.
In this problem, a building with N floors (for a constant N > 1 of your choice) has three elevators. On each floor there are three doors, one for each elevator, and two buttons labeled "up" and "down". Pressing either "up" or "down" on a given floor brings one of the three elevators to that floor. The "up" and "down" are hints to the elevator scheduler about which direction the person would like to travel. Pressing the "up" or "down" button causes that button to light up; pressing a button when it is already lit has no effect on the system. The "up" (resp. "down") button light goes out when an elevator traveling in the upwards (resp. downwards) direction arrives at that floor. Above each elevator on each floor there is a display showing the elevator's current travel direction.
Each of the three doors on each floor is controlled by a separate controller. When an elevator arrives at a floor, it can request that the controller open or close the door on that floor. A person can only enter the elevator when the door is open. Once a person enters an elevator, he/she can press one of N buttons (labeled 1 to N) inside the elevator to request that the elevator go to the corresponding floor. If the elevator's current direction is upwards on the ith floor, pressing buttons whose label is less than or equal to i has no effect. Conversely, if the elevator's current direction is downwards on the ith floor, pressing buttons whose label is greater than or equal to i has no effect. An elevator can change direction from up to down (resp. down to up) only when all floor requests for that elevator are less than (resp. greather than) its current floor.
You may assume that all the relevant hardware works perfectly without failures. You are to write a Promela model of the elevators, doors and elevator patrons. In addition, for each of the following properties you are to do the following (1) state whether it is a safety or liveness property, (2) express it as an LTL formula, and (3) use Spin to ensure that your model upholds the property:
Things to submit :
1. Your promela file, which you should include (a) your answer about whether each property is a safety or liveness property (b) your LTL formulae
2. You should also hand in each LTL encoding as a separate file. File names should be "formula_1.txt", "formula_2.txt", "formula_3.txt".
A common problem in the design of a distributed system is ensuring that there is consensus about a value among a set of processes. For instance, all the servers in your bank's computing system must agree about the amount of money in your checking account. The challenge in achieving consensus is that some of the relevant processes may be down for a time period and network connections might fail for a time period, preventing some of the processes from communicating with each other. Having a few processes or a few network connections down should not prevent the system as a whole from updating the value.
Lamport invented the Paxos algorithm to solve the consesus problem. You should first carefully read his paper "Paxos made simple", which describes the algorithm. The problem is to encode the Paxos algorithm in Promela. Your model must include the ability for processes to go offline and online (crash and reboot) and for network links to go offline and online. The second part of the problem is to design a set of safety and liveness properties that demonstrate that the Paxos algorithm does achieve consensus if sufficient amounts of the system are up and working. The properties you choose should, of course, not hold if too much of the system is down. You can encode your properties in any form that Spin can check, the most likely forms being assert statements and LTL formulae. Be sure that your Promela code includes comments that describe the properties informally in English and that describe your formal encoding. (For instance, if you used the LTL dialog box in Xspin, be sure to include a copy of the LTL formulae in your Promela comments.) The Promela file is the hand-in for this problem.
In lecture, I described a naive Zing model of banking. I first showed how the whole system can be encoded as a single Zing model, which allows Zing to check whether the whole system is stuck-free. Then I showed how we can check the same stuck-freedom compositionally by giving each component an interface and by using Zing to check (1) that each component implements its interface and (2) that each component, implemented only in terms of other components' interfaces, is stuck-free. In particular, using CCS notation, we first described a system
Sys = Atm | Branch | Bank
and used Zing to ensure that Sys is stuck-free. Then we showed compositionally that Sys is stuck free by using Zing to show the following:
(Because this example is a toy, Zing takes longer to show these five conditions than to test directly whether Sys is stuck-free, but for a realistic system, this is not the case. Indeed, directly checking whether the whole system is stuck-free is often infeasible.)
This problem is to elaborate the banking model and to show that the resulting, more complicated model is still stuck-free both non-compositionally and compositionally. Here are the complications to add:
3A. You should begin by changing the whole-system Zing specification from lecture to account for these new compilications. Then use Zing to ensure that your whole new model is stuck-free.
3B. Next you will need to show compositionally that the system is stuck-free. Namely, you will need five Zing files that represent the following pieces:
For Zing's conformance checker, event-based interaction is considered exported public behavior, whereas channel-based interaction is considered a hidden part of a process's algorithms. Hence a conformance check tests whether an implementation's event interactions are compatible with an interface's event interactions. As a result, you will need two versions of both IBranch and IBank. The version of IBranch in file 1 above is implemented in terms of events because it's used for a conformance check. The version of IBranch in file 5 is implemented in terms of channels because it's part of the Atm implementation. Similarly, the version of IBank in file 2 is implemented in terms of events because it's used for a conformance check. The version of IBank in file 4 is implemented in terms of channels because it's parts of the Branch implementation. (The tedium of the repeated definitions is because Zing is used as the back-end of a compiler, which automatically produces the two versions that we must produce by hand.)
Zing can be downloaded from the Microsoft Research web site. The Zing team has very kindly given us a pre-release version to play with ahead of its scheduled release date. As a result, this tool is not as well tested as the other tools you'll use in class. If you experience any crashes or other bugs, please let me (Rob) know and I'll give a bug report to the Zing team. The Zing team is generally very responsive to bug reports, which means that you should be prepared to uninstall Zing and download new versions from the web site, in order to pick up bug fixes. If such bugs arise, I'll post to the course mailing list.
As with assignment 1, you should hand in your assignment both using E-Submit and on paper in lecture. For the paper copy, please print out all three problems as three separate documents, each of which has your name on in and is stapled together. The three stapled documents should then be paper-clipped together and handed in. This arrangement allows Miryung and I to split up the hand-ins by problem and to grade them in parallel. Your cooperation in this little bit of bureaucracy is greatly appreciated!