
View Module
General Information
Software Requirements: Simple Formal Modeling (REQ2) 
Version
1
, submitted by
sebern
on
3/8/2003
at
12:00 AM
View Revision History 
sebern.2003.1 
This module is designed to introduce the analysis and specification of software requirements using simple formal techniques and the Z notation. It is intended as preparation for more extensive use of formal methods of requirements analysis, specification, and verification. This module minimizes the complexity of requirements elicitation by using an example with which students should already be familiar, and uses the same example found in module REQ01 (informal specification). 
Lecture: 2 hours
Exercise: 23 hours

This 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. A primary purpose of this module on simple formal specification show students how formal methods can be used to compensate for some of the weaknesses inherent in informal specifications. 
SEEK Categories

Modeling foundations
(MAA.md)
Authors

Mark Sebern
Prerequisites

Proficiency in programming in a highlevel language.

Experience in design of small software systems.

Familiarity with informal software requirements specifications.

Familiarity with Z formal notation.

Familiarity with simple LaTeX document preparation.

Basic proficiency with Z/EVES syntax checker and theorem prover functions.
Learning Objectives

Knowledge

Describe how a formal notation like Z can be used to model software requirements.

Synthesis

Model and document software requirements in a simple formal specification.

Analysis

Use a Z theorem prover to identify inconsistent or incomplete software requirements expressed in formal notation.

Evaluation

Identify difficulties encountered in analyzing and specifying software requirements using the Z formal notation.
Topics

Techniques used in formal specification of software requirements.

Analysis and simple formal specification of software requirements.

Benefits of applying formal techniques to the modeling and analysis of software requirements.
Materials

Teaching tips for the REQ02 module
(HTM)
0.00/5
[Rate Material]

REQ02 exercise
(HTM)
0.00/5
[Rate Material]

Skeleton Z model file
(TEX)
0.00/5
[Rate Material]

Sample soluton Z model file
(TEX)
0.00/5
[Rate Material]
See Also...
No alternate modules.
Other Resources

Jacky J.. The Way of Z: Practical Programming with Formal Methods, Cambridge University Press, 1997.

Diller A.. Z: An Introduction to Formal Methods, Second Edition, John Wiley & Sons, 1994.

Z/EVES syntax checker and theorem prover
(Link)

SWEBOK
(Link)

Bourque P. and Dupuis R., eds. Guide to the Software Engineering Body of Knowledge, IEEE CS Press, Los Alamitos, Calif., 2001.
Ratings
Log in to
rate this module.
Discussions
Discuss this module in the forums.
