Click here to access press info

Models of Software Systems

Where you learn how to formally model and reason about software systems


Scientific foundations for software engineering depend on the use of precise, abstract models for characterizing and reasoning about properties of software systems. This course introduces various 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 definitions and denotational descriptions are themes of the course.

After completing this course, students will be equipped to:
› Understand the strengths and weaknesses of certain models and logics, including state machines, algebraic and process models, and temporal logic
› Select and describe appropriate abstract formal models for certain classes of systems
› Describe abstraction relations between different levels of description, and reason about the correctness of refinements
› Prove elementary properties about systems described by the models introduced in the course.




"... in situations where correctness [is] paramount, such as the software that runs heart pacemakers or nuclear power plants [the use of] formal methods can be justified : one [can] move from formal specifications of a system to a probably correct implementation of it."


David Garlan, Jeanette Wing and Orietta Celiku, "Models of Software Systems"