(This is a tentative course syllabus. Everything in this document is subject to arbitrary change without notice.)
Bart Massey <firstname.lastname@example.org>
Warren Harrison <email@example.com>
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.
The Way Of Z
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
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:
Three quizzes will be given at the dates indicated on the schedule below:
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
*# = Homework assigned, # = Homework due
|Introduction To Formal Methods||FM1; Z 1-4|
|*1||Sets, Graphs, Logic, Proofs, and Programs||FM 2; Z 8-11,D,E|
Introduction To Z
|More About Z||Z 12-15|
|3||FSMs and State In Z|
|Schemas and Birthday Books
|FSMs In Testing
A Z Application
Jane Pan: The Airbus Cabin System
|FM 4, 11|
|TBA; FM 17|