Software Modeling Process SWEN 4321

Course description:

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, and inductive and denotational descriptions are recurrent themes throughout the course. 

Course Aims:

The aims of this module are to:
  • illustrate the strengths and weaknesses of certain models and logics including state machines, algebraic and process models, and temporal logic;
  • 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.

Course outcomes:

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.