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 Instructors:**

Bart Massey<bart@cs.pdx.edu>

Warren Harrison<warren@cs.pdx.edu>

**Prerequisite:**

OMSE 500: Principles of Software Engineering

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.

- Basic knowledge of or experience with discrete mathematics normally obtained via an undergraduate course in the subject.
- Basic practical software engineering knowledge, normally obtained via OMSE 500, Principles of Software Engineering.

Students should:

- Understand the role of mathematical and formal methods in modeling and analysis of software systems.
- Understand the standard methods and notations of set theory, formal logic, automata theory, and graph theory.
- Understand the Z formal specification notation, and be able to use it to specify and validate real software systems.
- Understand the application of formal models and analysis to a variety of real software engineering projects.

Quizzes | 30 |

Homework | 40 |

Final Presentation | 25 |

Class participation | 5 |

TOTAL | 100 |

*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

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.*

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

- Review of sets, graphs, functions, logic, proofs, and programs.
- Simple Z descriptions.
- Advanced Z descriptions.

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

- Quiz on sets, graphs, logic, proofs, and programs.
- Quiz on Z.
- Quiz on formal methods applications.

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.

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.

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

*(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 1Introduction 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 BooksQuiz 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 |
PresentationQuiz 3Concluding Comments |
TBA; FM 17 |