Models of Software Systems

Recommended Prerequisites

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

Teaching Methods

This course will include theoretical lectures with detailed exposition of concepts, principles and fundamental techniques of formal modelling, along with practical examples intended to increase students' interest in theoretical concepts and exemplify their application to real situations.
To allow more time to answer questions, and to cover certain topics in greater depth there are weekly "recitation" sessions. The course is organized around weekly homework assignments and a set of 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) capably prove elementary properties about systems described by the models introduced in the course.

Work Placement(s)

No

Syllabus

- Introduction: course info; what a model is.

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

- State machines; FSP; reasoning about state machines.

- Introduction to Z; Z techniques and examples; refinement and abstraction.

- Introduction to concurrency; concurrent state machines; FSP modeling techniques; reasoning about

concurrency.

- Linear Temporal Logic; automated reasoning.

- Formal methods in the real world; introduction to Petri Nets; reasoning about Petri Nets; UML.

Head Lecturer(s)

Raul André Brajczewski Barbosa

Assessment Methods

Assessment
Midterm take-home exam: 15.0%
Exam: 25.0%
Three group projects : 30.0%
homework assignments : 30.0%

Bibliography

- FAA En Route Resectorization - A Formal Specification. V.J. Harvey, and P.R.H Place. Unpublished manuscript, September 1999.

- Coloured Petri Nets: A High Level Language for System Design and Analysis. K. Jensen. In High-level Petri Nets: Theory and Application. K.

Jensen and G. Rozenberg (eds.) Springer-Verlag, 1991.

- Temporal Logic Draft version of chapter from book in preparation. 1996.

- Concurrency: State Models and Java Programs. J. Magee and J. Kramer.

Wiley, 1999.

- Petri Nets. J. L. Peterson. ACM Computing Surveys, Sept 1977.UML Walkthrough. J. Rumbaugh, I. Jacobson, and G. Booch. In The Unified Modeling Language Reference Manual.  Addison Wesley, 1999, pp. 25-39.

- An Introduction to Z and Formal Specification, J. M. Spivey. SW Eng Journal, pages 40-50, January 1989.

- Using Z: Specification, Refinement, and Proof. J. Woodcock and J. Davies.

Prentice-Hall International, 1996.

- Software Engineering Mathematics. J. Woodcock and M. Loomis, Addison-Wesley 1988.

Livros obrigatórios | Required textbooks:

- Models of Software Systems, D. Garlan, J. Wing, O. Celiku, and D. Kroening, 2010.

- Concurrency: State Models and Java Programs, Magee and Kramer, 1999.

Referências opcionais | Optional references:

- The Z Notation: A Reference Manual, 2nd Edition, J. M. Spivey.

- Logic in Computer Science, Modelling and Reasoning about Systems, Huth and Ryan.

Literatura suplementar | Supplemental handouts:

- Concepts and Notations for Concurrent Programming, Andrews and Schneider. Computing Surveys, Vol. 15, No. 1, March 1983.

- Formal Methods: State of the Art and Future Directions, Edmund M. Clarke and Jeannette M. Wing, report by the Working Group on Formal Methods for the ACM Workshop on Strategic Directions in Computing Research, ACM Computing Surveys, vol. 28, no. 4, December 1996, pp. 626-643.

Also CMU-CS-96-178.

-  Statecharts: a visual formalism for complex systems. D. Harel. Science of Computer Programming, 8:231-274, 1987.