Models of Software Systems

Credits: 12 units

Semester: Fall

Length: full semester


How to gain confidence in correctness of the software that runs airplanes or medical devices? If we consider the overall costs of maintenance and rework due to error, producing software using formal methods more than made up for higher costs at the front end of the software life cycle.

That’s why this course treats foundations for software engineering based on the use of precise, abstract models and logics for characterizing and reasoning about properties of software systems. Also 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 definitions and denotational descriptions are recurrent themes throughout the course.

This course provides the formal foundations for the other core courses. Notations are not emphasized, although some are introduced for concreteness. Examples are drawn from software applications.

More course details can be found in the Models of Software Systems syllabus.

After completing this course, students will be able 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.
  • Reason about the correctness of model refinements.
  • Prove elementary properties about systems described by the models introduced in the course.
  • Understand prerequisite mathematical foundations for the other core courses.


Undergraduate discrete math including first-order logic, sets, functions, relations, proof techniques (such as induction).

Сайт находится в технической разработке