MIT

Final Project

Your final project is an opportunity to explore ideas we've studied more deeply, to get some experience with a more realistic practical application, or to learn about an approach that we haven't covered but which fits within the purview of the course.

You'll do your projects in groups of 2 or 3 students. There are 3 deliverables:

  1. By 10am Wednesday, April 27: a 1-2 page proposal outlining what you plan to do. The purpose of this is to focus your project and give us an opportunity to guide you and ensure that your project will be rewarding and constructive. Your proposal should have the following parts: (1) an overview of the problem you plan to investigate; (2) an explanation of why the problem matters, and what you expect to learn from it; (3) a list of risks that you anticipate (problems that may arise) and how you expect to respond to them. We will respond to your proposal within a day or two.

  2. By 5pm Friday, May 6: a draft slide presentation of your project results, to be presented in its final version in class the following Monday or Wednesday. We are asking for draft presentations in advance so we can give you some feedback and ensure that the final presentations are as useful and constructive as possible. Each group will have about 15-20 minutes, so you should plan no more than 10 slides, and should focus on explaining some substantial ideas, rather than attempting to give a broad but shallow overview.

  3. By 10am Wednesday, May 11: the final project report. It should include at least the following sections: (1) an abstract of no more than 200 words summarizing what you did; (2) an introduction explaining the problem and its motivation; (3) a technical summary of what you did; (4) a critical evaluation: what you learned about the problem and about the approach you used; (5) references to any papers or books or websites cited; (6) appendices containing in full any models, specifications or code that you produced. Your report should be no less than 3 pages in length and no more than 10, excluding appendices.

Project Ideas

Here are some ideas to help you get started thinking about possible projects.

  1. Take a design or spec that's already described in some detail in a published paper and build a formal model and analyze it using Alloy or a model checker. For example,

    • N. Feamster, J. Winick, and J. Rexford. A Model of BGP Routing for Network Engineering. Proc. ACM SIGMETRICS, New York, NY, June 2004 (pdf)

    • Bonjour Technical Specification. Apple Computer (pdf)

    • S. Gavrila, J. Barkley. Formal Specification for Role Based Access Control User/Role and Role/Role Relationship Management. (1998), Third ACM Workshop on Role-Based Access Control. (pdf). See other papers at (website)
  2. Construct a series of small models for some course material in computer or software systems, to make the material more precise, and to clarify and crystallize the key properties. For example, you could take one of the chapters of the 6033 text on memory hierarchy, naming or transactions: all should be fairly straightforward to express and analyze with Alloy or a model checker. The course notes for 6.826 (Principles of Computer Systems) include many interesting examples already expressed in SPEC, a formal language; you could translate some examples into a checkable language and do some analysis. (website)

  3. Construct and analyze a metamodel to investigate some aspect of formal analysis. For example, you could model the abstraction function method with a state machine and a trace semantics, and show that if an abstraction function exists, you have trace inclusion. Or perhaps you could model the semantics of LTL and CTL, and show that certain formulas imply others.

  4. Learn how to use a new tool, experiment with it on some small examples, and compare it to the tools you've seen. We recommend in particular:

    • The SPIN model checker, which accepts LTL specs and has a modelling language based on guarded commands, written in a C-like notation;
      (website)

    • The LTSA verification tool, which is based on a process algebra called FSP; a very different formalism than the ones we studied, but a very nicely packaged tool with lots of good examples (and a book to go with it that I can lend you);
      (website)

    • The Bogor model checker, which offers a high-level modelling language and a pluggable architecture
      (website)
  5. Investigate a novel application of analysis technology. For example, it should be possible to use Alloy to check Hoare logic proof outlines. You could do this for an object-oriented program, by representing instance variables as relations.

Please recall the somewhat enthralling submission instructions.