OMSE 522: Modeling and Analysis of Software Systems
Tentative Course Syllabus

Bart Massey and Warren Harrison
Oregon Master of Software Engineering
Spring 2000

(This is a tentative course syllabus. Everything in this document is subject to arbitrary change without notice.)

Course Information

Course Number: OMSE 522
Course Title: Modeling and Analysis of Software Systems
Credits: 3
Offer Date: Spring 2000
Meeting Time: Tuesday, 6:00PM-8:50PM

Course Instructors:

Bart Massey <bart@cs.pdx.edu>
Warren Harrison <warren@cs.pdx.edu>

Prerequisite:

OMSE 500: Principles of Software Engineering

Course Description

Abstract models are used to formalize specifications of software systems. Formalized reference specifications serve as a basis for the design of software implementations and for validating critical properties of software systems. This course provides the fundamental mathematical concepts needed to understand abstract models of software and to reason about them as well as examples showing how they are applied.

This quarter we will be taking a look at formal notations, especially the Z formal specification notation. In the process of understanding these notations and applications, we will learn and recover basic concepts in mathematical and formal analysis. This material will be interleaved with the discussion of real-world case studies in applications of these techniques to domains such as hazardous materials handling, telephone switching, railway signalling, and instrumentation.

Course Aims and Objectives

Preconditions

Postconditions

On completion of this course students will be able to use common formal software development methods, and will understand the role of formal methods in real-world software engineering.

Students should:

Measuring Student Progress

Quizzes 30
Homework 40
Final Presentation 25
Class participation 5
TOTAL 100

About The Course

Course Texts

The Way Of Z
Jonathan Jacky
Cambridge 1997
ISBN 0-521-55041-6 [hardback]
ISBN 0-521-55976-6 [paperback]

Applications of Formal Methods
Michael G. Hinchey and Jonathan P. Bowen, eds.
Prentice Hall 1995
ISBN 0-13-366949-1

Instructions

You are expected to be in class for all sessions and to be on time. You must read all assignments prior to class so that you can get maximum benefit from each session; the readings and projects will require more time than you think. If you are forced to miss class due to work or illness, please make arrangements with your professor before you miss to work out a plan to make up missed sessions. Always contact your professor as soon as possible if you need help or have any questions.

Readings are assigned each week. You are expected to complete the readings in advance, and relate them to the lecture material. In addition, you are required to complete a series of course assignments. All projects are due at the stated time: no late assignments will accepted and no make-up exams will be given, except in pre-arranged and emergency situations.

Coursework

A variety of methods will be used to aid and evaluate progress in the course.

Homework

Three homework assignments will be given out at dates indicated on the schedule below:

  1. Review of sets, graphs, functions, logic, proofs, and programs.
  2. Simple Z descriptions.
  3. Advanced Z descriptions.
Homework grades will be strictly on a pass/fail basis; the homework is primarily for the benefit of the student.

Quizzes

Three quizzes will be given at the dates indicated on the schedule below:

  1. Quiz on sets, graphs, logic, proofs, and programs.
  2. Quiz on Z.
  3. Quiz on formal methods applications.

Final Presentations

Each student will present a paper from the Formal Methods book (or elsewhere) during week 8 or 9 of class, and will write a short paper on the topic addressed.

Academic Honesty

You will receive a document in class detailing OMSE policy on academic honesty. Please contact your instructors if you have any doubts about the propriety of your course activities.

Class Participation

Your class participation grade will be based on your attendance and participation in the class discussion periods.

Course Schedule (Spring 2000)

(Z = The Way Of Z, FM = Applications of Formal Methods)
*# = Homework assigned, # = Homework due

Lecture HW Topics Readings
1: 3/28
  Introduction To Formal Methods FM1; Z 1-4
2: 4/04
*1 Sets, Graphs, Logic, Proofs, and Programs FM 2; Z 8-11,D,E
3: 4/11
1,*2 Quiz 1
Introduction To Z
Z 5-7
4: 4/18
  More About Z Z 12-15
5: 4/25
2,*3 Tutorial Session  
6: 5/02
3 FSMs and State In Z  
7: 5/09
  Schemas and Birthday Books
Quiz 2
FM 4
8: 5/16
  FSMs In Testing
A Z Application
Jane Pan: The Airbus Cabin System
FM 4, 11
9: 5/23
  Presentations TBA
10: 5/30
  Presentation
Quiz 3
Concluding Comments
TBA; FM 17