CSSE 373 Formal Methods in Specification and Design

P3

Administrative Details

Purpose: practice modeling a system using JML

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-201130-teamNN

  where NN is your assigned team number.

• Keep track of how much time you spend on this assignment.
• You will submit your solution by committing a documented Eclipse project to your team repository.
• There is no separate report for this milestone.
• This is the first time this project has been assigned. Please be sure to ask me questions if you’re confused about anything. The odds of errors in the simulator are fairly high; I didn't formally verify the simulation.

Problem Specification

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

• the buttons (and their illumination)
• the lifts (including their direction arrows, e-stops, etc.)
• the requests
• the controller algorithm

I'm providing a simulator for the hardware and for the humans who would push buttons in the lifts. I'm also providing a text-based view of the system that displays its state.

You will annotate two classes, control.LiftController and control.FloorController, with JML specifications, test them using JMLUnitNG, and run the simulator using these classes.

Tasks

1. In Eclipse, check out the HigherExpectations project from your project team SVN repository.

2. Study the provided code, noting the following:

   • The build.xml file includes targets for:

     • generating JMLUnitNG tests,
     • compiling the whole project with plain old Java,
     • running the simulation with plain old Java,
     • running the simulation using run-time assertion checking, and
     • running JMLUnitNG tests of both FloorController and LiftController.
   • The simulation is started in the class main.Main. This class creates instances of LiftSimulator, which simulate the hardware of a lift car, and instance of FloorSimulator, which simulator the buttons in the hallway for calling a lift in a particular direction. For each simulator, Main also creates an instance of your LiftController or FloorController as appropriate.
   • Each LiftController knows about its LiftSimulator, and vice versa. This lets the simulator tell the controller when an event occurs, such as a button press or arriving at a floor. This arrangement also lets the controller tell the simulator to open the lift door, or start moving up, etc.
   • Each FloorSimulator knows about its FloorController. This lets the simulator tell the controller when a button has been pressed.
   • Every FloorController knows about every LiftController. This lets the floor controller tell all the lifts when a floor call button has been pressed.
   • Every LiftController knows about every FloorController. This lets the lift controller poll all the floors looking for pending floor call requests.

3. Your primary task is to add JML specifications to control.LiftController and control.FloorController, implement and test them using JMLUnitNG, and run the simulator using these classes.

   Annotate the class as follows:

   1. Add appropriate fields for tracking the state of the lift or floor.
   2. Add appropriate invariants to the class.
   3. Specify each public method, plus the constructor of the class. Each specification should include:
      • a pre-condition
      • an assignable clause
      • a post-condition

      To guide you, the ILiftController and IFloorController interfaces provide informal, javadoc descriptions of all the methods. Also, note that the interfaces include initially clauses that constrain your constructors.

      You may also find your (or my) Alloy model from P2 useful. I did.

   4. Implement the methods, introducing helper methods as needed.

   The simulator is designed to throw an exception and stop the simulation if your control algorithm makes an illegal request, such as asking a lift to move while its doors are open, open its doors while its moving, or do anything while out of service. Your controller will have to track the state of the system to avoid making such requests.

Rubric

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

Turn In

Turn in your work by committing your Eclipse project to your team repository.