REQ02 Teaching Tips
Simple Formal Requirements Specification
Developed with support from the National Science Foundation
Draft version 0.1
The REQ02 module is appropriate for inclusion in a first course in software requirements
or in a course that applies formal methods to the documentation and analysis of
software requirements. The example used in the module exercise can also be used as
a vehicle to work with informal specification and modeling, as in module REQ01.
It is assumed that LaTeX and Z/EVES have already been installed on computer systems to be
used in completing the exercise, and that students have experience with using these
The LaTeX style file distributed with Z/EVES is required
for proper rendering of the specification.
This module is designed to be presented in two class sessions, with the exercise done
between the two sessions. The first session presents the skeleton specification and exercise,
leading into a class discussion to prepare for the exercise. The second session
follows up on the completed exercise, using the sample solution as a guide.
In the first class session,
distribute the REQ02 exercise to the students.
If they have not already completed module REQ01, briefly (10 minutes) present the
system description, clarifying terminology and system components. It may be helpful
to draw diagrams of the buttons and indicators inside the elevators and on each floor.
Present the skeleton Z specification, pointing out the key elements.
In the second class session, after the exercise reports have been submitted
(and, if possible, evaluated),
the instructor should identify areas of potential or actual difficulty in completing the exercise,
and discuss the experience with the students. The sample solution may be used to provide suggestions
for dealing with problems encountered by the students.