Models of Software Systems

Recommended Prerequisites

Discrete mathematics including first-order logic, sets, functions, relations, proof techniques (such as induction).

Teaching Methods

This course includes theoretical lectures with detailed exposition of concepts, principles and fundamental techniques of formal modelling, along with practical examples to increase students' interest in theoretical concepts and exemplify their application to real situations. To allow for more time to answer questions there are weekly "recitation" sessions. These sessions are practical in nature and suitable to take a closer look at the homework exercises and the projects. The course is organized around weekly reading assignments, with homework exercises, and three group projects.

Learning Outcomes

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.

After completing this course, students will (i) understand the strengths and weaknesses of certain models and logics including state machines, algebraic and process models, and temporal logic, (ii) be able to 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, and (iii) prove elementary properties of modeled systems using techniques introduced in the course.

Work Placement(s)

No

Syllabus

- Introduction: course information; what a model is.

- Foundations: logic; proof techniques; sequences; sets, relations, and functions.

- Discrete event systems; finite-state machines; reasoning about state machines.

- Introduction to model checking; verification of sequential programs.

- Concurrency; concurrent state machines; modeling techniques; reasoning about concurrency.

- Linear Temporal Logic; safety and liveness properties; automated reasoning and formal verification.

- Modeling distributed systems; reasoning about communicating processes.

- Formal methods in the real world.

Head Lecturer(s)

Raul André Brajczewski Barbosa

Assessment Methods

Assessment
Exam: 30.0%
Project: 70.0%

Bibliography

Livros essenciais | Required textbooks:

- Introduction to Discrete Event Systems, C. G. Cassandras et al., Springer, 2008.

- Principles of the Spin Model Checker, M. Ben-Ari, Springer, 2008.

Opcional | Optional:

- Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth et al., Cambridge, 2004.

- Concurrency: State Models and Java Programs, J. Magee et al., 2nd Ed., Wiley, 2006.

- The Spin Model Checker: Primer and Reference Manual, G. J. Holzmann, Addison-Wesley, 2004.

- Verificação de Modelos, R. Barbosa, 2018.

Suplementar | Supplemental:

- Concepts and Notations for Concurrent Programming, G. R. Andrews et al., Computing Surveys, Vol. 15, No. 1, 1983.

- Formal Methods: State of the Art and Future Directions, E. M. Clarke et al., ACM Computing Surveys, Vol. 28, No. 4, 1996.

- A Primer on Model Checking, M. Ben-Ari, ACM Inroads, Vol. 1, No. 1, 2010.

- The Model Checker Spin, G. J. Holzmann, IEEE Transaction on Software Engineering, Vol. 23, No. 5, 1997.