Models of Software Systems
Administration
Instructors: David Garlan and
Jeannette Wing
TA: James Ivers
Secretary: Cary Lund
Objectives
Scientific foundations for software engineering depend on the use
of precise, abstract models and logics for characterizing and reasoning
about properties of software systems. There are a number of basic
models and logics that over time have proven to be particularly
important and pervasive in the study of software systems. This course
is concerned with that body of knowledge. It considers many of the
standard models for representing sequential and concurrent systems,
such as state machines, algebras, and traces. It shows how different
logics can be used to specify properties of software systems, such as
functional correctness, deadlock freedom, and internal consistency.
Concepts such as composition mechanisms, abstraction relations,
invariants, non-determinism, inductive and denotational descriptions
are recurrent themes throughout the course.
By the end of the course you should be able to understand the
strengths and weaknesses of certain models and logics, including state
machines, algebraic and trace models, and temporal logics. You should
be able to apply this understanding to select and describe abstract
formal models for certain classes of systems. Further, you should be
able to reason formally about the elementary properties of modeled
systems.
Contents
Resources
![[ Previous ]](http://www.cs.cmu.edu/~norm/msd/images/previous_motif_gr.gif)
![[ Next ]](http://www.cs.cmu.edu/~norm/msd/images/next_motif_gr.gif)
![[ Contents ]](http://www.cs.cmu.edu/~norm/msd/images/contents_motif_gr.gif)
![[ Up ]](http://www.cs.cmu.edu/~norm/msd/images/up_motif_gr.gif)
The text, images, and information in this document are copyright Carnegie Mellon Univeristy Computer Science unless stated otherwise.
Comments about the pages themselves? Direct them to the WebMaster of this page.*