REQ02 Teaching Tips

Simple Formal Requirements Specification

Developed with support from the National Science Foundation

Draft version 0.1


  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.
  2. 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 tools. The LaTeX style file distributed with Z/EVES is required for proper rendering of the specification.
  3. 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.
  4. 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.
  5. Present the skeleton Z specification, pointing out the key elements.
  6. 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.