CSSE 373 Formal Methods in Specification and Design

P4

Administrative Details

Purpose: practice modeling a complex reactive system with statecharts

Please note: A big part of practical formal methods is having conversations with your client so that your model reflects what they really want. To give you practive with that, projects in this class are somewhat underspecified and require that you go somewhat beyond what is specifically covered in class. I look forward to helping you with that, which is why some class meetings are canceled for project work, but you need to ask for help.

Other details:

• You must work in teams of 2 or 3 on the projects.

• Your team has a Subversion repository for the projects. The repository URL is:

  http://svn.csse.rose-hulman.edu/repos/csse373-201030-teamNN

  where NN is your assigned team number.

• Keep track of how much time you spend on this assignment.
• You will submit your solution as a report in pdf format.

Problem Specification

Your task is to construct a statechart model of the lift system from P2 that describes:

• the buttons (and their illumination)
• the lifts (including their direction arrows, emergency stop, etc.)
• the requests
• the controller algorithm

Requirements

1. Construct a statechart model of the lift system. For full credit your solution must:

   • Use the higher order features of statecharts. Examples include orthogonal statecharts (separated by dashed lines), nested statecharts, and history.
   • Obey the laws of physics. For example, lifts must pass through intervening floors rather than "teleporting" past floors.
   • Be professionally presented—scanning hand-drawn sketches is not acceptable.
   • Include a clear description of the events and states of the system. You may find that tables are a good way to present this information.
   • Include the names of all team members and the team name.
2. You will submit a pdf document of your solution. Individual sub-diagrams should not span multiple pages. That is, a transition arrow must not begin on one page and end on another. Pages should be no larger that 8 1/2 x 11 inches.

Suggestion

You may use whatever tool your team finds most useful for drawing your diagrams. The Macs in the CSSE labs have the OmniGraffle program, which is quite nice for this sort of work. See me if you would like a quick demo. OmniGraffle will export in a variety of formats, including images that you could embed in Word or LaTeX documents.

Rubric

I will evaluate your work using this grading rubric [pdf].

Turn In

Turn in your work by committing your pdf document to your team repository.