SWEnet
Home  |  Wiki  |  About  |  Search  |  Advanced Search  |  Forums Login  |  Register

View Module

An error occurred while attempting to get the requested module. Cannot open database "AspNetForums" requested by the login. The login failed. Login failed for user 'swenet'. at AspNetForums.Data.SqlDataProvider.GetRatingForUser(String username, Int32 parentID) at AspNetForums.Ratings.GetRatingForUser(String username, Int32 parentID) at SwenetDev.ModuleRatingsControl.getRatingForUser(String username, ModuleRatingInfo ratingInfo) at SwenetDev.viewModule.Page_Load(Object sender, EventArgs e)

General Information

Title Software Requirements: Simple Formal Modeling (REQ2)
Version Info Version 1 , submitted by sebern on 3/8/2003 at 12:00 AM
View Revision History
Module Identifier sebern.2003.1
Abstract 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).
Size Lecture: 2 hours
Exercise: 2-3 hours
Comments 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

  1. Modeling foundations (MAA.md)

Authors

  1. Mark Sebern

Prerequisites

  1. Proficiency in programming in a high-level language.
  2. Experience in design of small software systems.
  3. Familiarity with informal software requirements specifications.
  4. Familiarity with Z formal notation.
  5. Familiarity with simple LaTeX document preparation.
  6. Basic proficiency with Z/EVES syntax checker and theorem prover functions.

Learning Objectives

  1. Knowledge - Describe how a formal notation like Z can be used to model software requirements.
  2. Synthesis - Model and document software requirements in a simple formal specification.
  3. Analysis - Use a Z theorem prover to identify inconsistent or incomplete software requirements expressed in formal notation.
  4. Evaluation - Identify difficulties encountered in analyzing and specifying software requirements using the Z formal notation.

Topics

  1. Techniques used in formal specification of software requirements.
  2. Analysis and simple formal specification of software requirements.
  3. Benefits of applying formal techniques to the modeling and analysis of software requirements.

Materials

  1. Teaching tips for the REQ02 module (HTM) 0.00/5 [Rate Material]
  2. REQ02 exercise (HTM) 0.00/5 [Rate Material]
  3. Skeleton Z model file (TEX) 0.00/5 [Rate Material]
  4. Sample soluton Z model file (TEX) 0.00/5 [Rate Material]

   

See Also...

No alternate modules.

Other Resources

  1. Jacky J.. The Way of Z: Practical Programming with Formal Methods, Cambridge University Press, 1997.
  2. Diller A.. Z: An Introduction to Formal Methods, Second Edition, John Wiley & Sons, 1994.
  3. Z/EVES syntax checker and theorem prover (Link)
  4. SWEBOK (Link)
  5. Bourque P. and Dupuis R., eds. Guide to the Software Engineering Body of Knowledge, IEEE CS Press, Los Alamitos, Calif., 2001.

Ratings

Number of Ratings:   0

Log in to rate this module.


Discussions

Discuss this module in the forums.

Related Modules