Simple Formal Requirements Specification Exercise
Developed with support from the National Science Foundation
Draft version 0.1
Introduction
The purpose of this exercise is to understand and extend a simple formal requirements
specification for a software system.
Assignment details
Introduction
Because this exercise concentrates on the specification and documentation of
requirements, rather than on eliciting them from clients or stakeholders, the
problem domain is one that you should already be familiar with. You are expected
to take into account your own knowledge of the problem domain in completing this
work.
You may complete this exercise by yourself, but it is preferable to work
as a member of a team (2-3 members).
If you do this, your colleagues may have differing views about the requirements
and how to best model them in Z.
You should reach some kind of consensus about the requirements and document them
as well as you can. There is more than one possible "right answer" for
this project.
System description
Study this overview of the system you are to specify. It is taken from a
similar problem addressed at the Fourth International Workshop on Software
Specification and Design, April 3-4, 1987, Monterey, California.
-
An n-elevator system is to be installed in a building with m floors. The
elevators and the control mechanism are supplied by the manufacturer. The
internal mechanisms of these are assumed (given).
-
The problem concerns the
logic to move elevators between floors according to the following
constraints:
- Each elevator has a set of buttons, one for each floor. These
illuminate when pressed and cause the elevator to visit the
corresponding floor. The illumination is cancelled when the
corresponding floor is visited by the elevator.
- Each floor has two buttons (except the top and bottom floors), one to
request upward travel and one to request downward travel. These buttons
illuminate when pressed. The illumination is cancelled when an elevator
visits the floor and is either moving in the desired direction or has no
outstanding requests.
- When an elevator has no requests to service, it should remain at its
final destination with its doors closed and await further requests. (An
alternative would be to specify a floor to which the elevator should
return under these conditions.)
- All requests for elevators from floors must be serviced eventually,
with all floors being given equal priority.
- All requests for floors within an elevator must be serviced
eventually, with floors being serviced sequentially in the direction of
travel.
- Each elevator has an emergency button that, when pressed, causes a
warning signal to be sent to the site manager. The elevator is then
deemed "out of service." Each elevator has a mechanism to
cancel its "out of service" status.
It is likely that you have are familiar with elevator systems similar to the one
described here. You should use your own experience to help you understand the details
of the system for which you are trying to specify the requirements.
Exercise Activities
-
Start with the skeleton Z model provided by the instructor
(LaTeX) (PDF).
-
Complete the specification of at least the following operations:
- MoveElevator
- VisitFloor
- ChooseDirection
Use the interface definition implied by each of these operations.
However, you may replace the skeleton schema with a schema of the same name
defined using the schema calculus (e.g., disjunction),
based on partial and supplementary operations.
The operation status codes (e.g., StatusOutOfService) are offered
as suggestions; you may modify them as you wish.
-
After importing your specification into Z/EVES and checking the syntax, attempt
to prove the "totality" theorems (that the precondition is met for all
possible inputs and states) for each of the above operations.
Include the proof steps in a "zproof" section of your LaTeX model file.
You will probably have some difficulty with the proofs, so start on them early
and ask the instructor for assistance.
You may get some ideas by running the proofs that are already provided for other
theorems in the skeleton model.
-
Edit the informal text of the specification as necessary, so the intent of your Z
model can be easily understood.
-
For extra credit, you may add other parts of the elevator system specification.
Be sure to supply appropriate informal text and proofs.
You may consult the instructor for suggestions.
-
Add a section to your specification describing any observations on the exercise,
difficulties you encountered, or questions that you still have.
If you have questions about the assignment, please consult the instructor.