CSSE 373 Formal Methods in Specification and Design

P3

Administrative Details

Purpose: practice modeling a system using JML

You may work in teams of 2 or 3 on the project.

Keep track of how much time you spend on this assignment.

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

You will submit Java files annotated with JML specifications.

Tasks

1. One team member should create a new Java project within his/her Mobius PVE workspace. Right-click the project and choose Team → Share Project to share this project to your team SVN repository. The other team members can check-out the project from there using the SVN Repository view in Eclipse.

   Be sure to use your team repository as for P1 and P2, even if you are working alone on the project milestones.

2. To get you started, here is a Java class modeling a single lift. Copy Lift.java into your workspace for this project. Annotate the class as follows:

   1. Add appropriate JML annotations to the fields of the class.
   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
3. Add and implement whatever classes you think are necessary to model the complete lift system from P2. You can use the style of Lift.java as a guide, but feel free to improve on that approach. Annotate the classes as described in the previous item.
4. Check all of your classes and specifications using ESC/Java2. Your goal should be to eliminate all ESC/Java2 warnings. If you are unable to do so, document each remaining warning with your best guess as to what’s wrong.

Suggestions

Don’t forget the crucial hints on using ESC/Java2 from HW10!

If this approach to modeling the lifts seems a bit odd, it may be helpful to think of this part as the Model in a Model-View-Controller implementation. We could make it into an actual such model by adding appropriate code to allow the View and the Controller code to observe the actions of the model. If we think about the problem this way, what is the View for this system in the real world? What is the Controller?

This is the first time I’ve assigned this milestone for the project. Please give me feedback as you go, so I can make adjustments as necessary. I’m not looking for any specific ”correct” answer; I’m just looking for a reasonable effort on your parts to understand how we might apply JML to this problem.

The original ESC/Java Users Manual might be a helpful resource.

Turn In

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

Feedback

Each team member should complete the short, anonymous survey on ANGEL regarding this assignment. (I will study these surveys in detail after the conclusion of this offering of the course. If you have suggestions that you would like me to consider during this offering of the course, please tell me in person or use the separate Anonymous Suggestion Box on ANGEL.)