Problem Set 3: Dynamic Alloy Model (due Mon April 4)
This is the second of a pair of assignments using Alloy to model a system of your own choosing. Whereas in the first assignment, you considered only static aspects, in this assignment, you'll build a model with dynamic behaviour. If you want to, you can extend the static model from the previous assignment, but you'll be expected to show a real increment, and to write a new report.
Your model should be presented as a self-contained case study. You should assume that your reader knows Alloy, but has no knowledge of the subject of the study. The writeup should include at least the following elements:
- (1) an introduction explaining what's being studied, and why it's interesting;
- (2) an informal overview of the subject, outlining the key concepts;
- (3) a detailed presentation of, and commentary on, the Alloy model;
- (4) a conclusion, explaining what was learned, and evaluating to what extent modelling and analyzing the subject was helpful.
Your model should include at least a couple of interesting simulations and at least one interesting assertion.
You should concentrate on developing the model, and only polish the writeup after the model is largely complete. The model should be small and simple: your aim is to capture the essence of your subject as succinctly as possible. As a rough guide, you should expect to develop a model that has at least 3 signatures and 3 fields, but no more than about 8 signatures and 12 fields. Use Alloy to help you check refactorings of your constraints to reduce them to a concise, elegant (and understandable!) form. If your model has become complicated and arcane, try and identify aspects of it that aren't essential, or try to find a way to take a more abstract view that will preserve the core content while removing extraneous detail.
When appropriate, you should make use of the patterns taught in lecture, and cite them when you use them: abstract state machine, declarative operation, local state, implicit invariant, invariant preservation, trace, etc. A rough draft of the book chapters on these patterns is available on the private readings page.
As examples of case studies developed by students with comparable experience in Alloy, see:
- Chord: A Peer-to-Peer Protocol by Hoeteck Wee
- Case Study in Alloy Modeling: A Common Profile for Presence by Edmond Lau
Both of these took several weeks of work, and involved extensive background reading. You should be less ambitious, and pick a subject that you already have some knowledge of, and can be confident you can model in a few hours. It's better to construct a simple model and polish it into something elegant and insightful than to construct a complicated model that you don't have time to rework.
You can pick any subject that appeals to you. Here are some suggestions:
- concurrency control: verify a schemes involving mutexes, semaphores, locks, etc. Consider questions about deadlock, livelock, and starvation. For a starting point, see Ilya Shlyakhter's model examples/algorithms/dijkstra.als, included in the Alloy release;
- Unix file system: model and analyze file system operations at the inode level; consider, for example, reclaiming unused blocks;
- caching strategies: specify a detailed caching strategy and show that it conforms to a simple, abstract, non-deterministic description;
- cellular automata: implement a cellular automaton framework in Alloy, and check theorems about it, or generate interesting cases. See Manu Sridharan's model examples/toys/life.als, included in the Alloy distribution.
- distributed algorithm: find a small algorithm, such as a leader election algorithm, and verify it;
- elevator: consider a bank of elevators with an arbitrary number of regular elevators and one or more freight elevators, serving an arbitrary number of floors, and characterize the desirable behaviours as a set of rules, as independent from one another as possible; [warning: this is a very hard problem!]
- style sheets: model the behaviour of hierarchical style sheets, as found in programs such as Word, InDesign, Quark, and Framemaker, paying attention in particular to how inheritance of formatting properties is handled, and to what happens when styles are deleted
- buffer management: model how applications typical handle multiple files, with buffers, recent file lists, etc;
- catalog views: model an application (such as iView Media Pro) in which assets (such as photos or email messages) can be classified in multiple ways, appearing in more than one folder at a time.
Appeal for volunteers: Prof. Darko Marinov (University of Illinois at Urbana-Champaign) is conducting some research on new Alloy analyses and has asked us to provide transcripts of Alloy modelling sessions. If you are willing to donate logs of your sessions to the cause of science, please do the following: (1) download the most recent nightly build of the Alloy analyzer; (2) turn on logging under the 'experimental options' tab of the preference settings; (3) email your log files directly to Darko at (marinov at cs.uiuc.edu). A small amount of extra credit will be awarded for furthering science.
Please recall the somewhat elusive submission instructions.