CSci 420/520: Project Proposal

Due Friday, October 28th by 1pm.

Summary

Write a proposal for your project that convinces the professor that the project is interesting and challenging.

Choosing a Project

Choose something that is interesting to you, and that has some degree of complexity and subtlety. Avoid systems that involve essential complexities that are difficult to specify. For example, you could specify two reals A and B where A < B, but it's more difficult to deal with floating point error issues for A + B == 1.

Ideas for a project:

• Find an existing specification and formalize it. Also formalize and check/prove properties of it. Examples: Microsoft's COM, Apple's Bonjour, USB 2.0, routing protocols, etc.
• Use a tool other than those in this course, such as SMV, SPIN, Z/Eves, LOOP, or Bogor. Compare it to the tools used in our class.
• Express the preconditions and postconditions for the data structures in CSci 241 using JML. Check the solutions provided by the book and/or instructor for correctness.
• Identify some critical and complex portion of a system you are working on for your research. Formalize it and check/prove interesting properties.
• Use a design by contract tool to augment an existing implementation with pre-conditions and post-conditions. Check the correctness of the implementation by subjecting it to a large number of inputs.

Writing the Proposal

Your writeup should contain at least the following:

• Identify all the people who will work on this project.
• A clear statement of what you intend to do. What problem are you trying to solve? Why does it require a formal approach?
• Landmarks to be met by the first status-report deadline.
• Criteria for successful completion of the project. How will you know when you are done?
• Discussions of any ideas you have about tools, modeling (e.g. logical representations), approach (e.g. a plan of attack), subtasks (e.g. who does what), and so forth.

Grading

150 points total.

Email a PDF of your proposal to meghan@cs.wm.edu.