CSci 435/535: Homework 8

Formal Methods

Due by Monday, April 11th by 11am

Summary

Work in pairs on this assignment. Feel free to use the forums to find a partner. Make sure the names of both students appear in the document. I will take a dim view on people who don't have a partner the day before the homework is due.

Develop a formal specification for the world, roads, road segments, lanes, and vehicles of our project. In addition to the state space of the software, you must also specify at least the transfer-vehicle-to-next-lane operation and the get-vehicle-in-front-of-this-vehicle operation. Extra credit will be given for additional specification effort, such as specifying multiple vehicle types, specifying (at a high level) the IDM or MOBIL models, or intersections.

You should not simply formalize the current implementation, but rather start over, thinking about how to represent the real world in an abstract way. For example, we have discussed already that the road segment contains an array of next lanes, but that this is probably not the best way to model the real world.

Writing the Specification

You will use the Z specification language to write your specification. There are a number of resources and examples on the course webpage. You may also wish to look at last year's specification of a billiards table: http://www.cs.wm.edu/~coppit/csci435-spring2004/homework/billiards_specification.pdf.

I have developed a LaTeX template to help you get started: http://www.cs.wm.edu/~coppit/csci435-spring2005/homework/specification-template-2005-04-04.tar.gz. To use the template, unpack it on one of the CS machines. Then edit source/simulator_specification.tex. When you want to view your specification, run make and open output/simulator_specification.pdf.

In terms of structure and exposition, your specification should explain each bit of formalism, and should explain unformalized or abstracted aspects of the system.

Type Checking

Your submission must type check correctly to receive any credit. You can easily check this by running make fuzz.

Questions

Post questions in the forum and I'll answer them as quickly as I can.

Submission

Run make dist and email me the resulting .tar.gz file.

Grading

300 points total. Both team members earn the same grade

You will be graded on completeness, correctness, structure/clarity, and appropriate structure and exposition.