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-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 by committing a documented Eclipse project to your team repository.

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.

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.

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.