Modelling and Validating Concurrent Systems
Objectives
1) To understand, describe and specify concurrent systems
2) To express safety and liveness properties of concurrent systems
3) To verify that the properties hold for the specifications
General characterization
Code
11560
Credits
6.0
Responsible teacher
António Maria Lobo César Alarcão Ravara, Carla Maria Gonçalves Ferreira
Hours
Weekly - 4
Total - 84
Teaching language
Português
Prerequisites
Basic knowledge of:
1) Programming
2) First-Order Logics
3) Set Theory
Bibliography
Main:
L. Lamport. The TLA+ Hyperbook http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html
L. Lamport. Specifying Systems. Addison-Wesley, 2002. http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf
C. Stirling. Modal and Temporal Properties of Processes. Springer, 2001. http://www.springer.com/us/book/9780387987170
Complementary:
L. Aceto et al. Reactive Systems: Modelling, Specification, and Verification. Cambridge University Press, 2007. http://rsbook.cs.aau.dk/
M. Huth and M. Ryan. Logic in Computes Science: modelling and reasoning about systems. Cambridge University Press, 2004. http://www.cs.bham.ac.uk/research/projects/lics/
Teaching method
Each week there is a two-hour lecture and a two-hour laboratory class.
Lectures include theoretical exposition, illustrated by case studies, and supported by the use of verification tools. In laboratory sessions, students solve exercises: modelling systems; specifying and verifying model’s properties.
Assessment includes two tests and two individual practical assignments. In both of the assignments, the student will have to model a concurrent system (these assessments differ on the complexity of the system being model), specify and verify a set of properties and write a report.
Conditions for approval: NE >= 9.5 and NT >= 9.5, where NE is the mean of tests grades and NT is the practical assignment grade.
Evaluation method
The evaluation elements are the following:
- 2 tests. The average grade of the tests will weigh 70% in the final grade.
- 2 projects. The average grade of the projects will weigh 30% in the final grade.
- Participation in lectures and lab classes may give a bonus of at most 10% in the final grade.
Note: The final exam, taken either for approval or grade improvement ("melhoria de nota"), will replace the tests component in the evaluation for the final grade.
To get frequency ("frequência") in the course it is necessary:
- Each project grade must be greater or equal to 7.0 points; and
- The average of grade of the projects must be greater or equal to 9.5 points.
Note: Students with frequency from previous year may may mantain it in the current year.
To get approved in the course it is required that:
- To have frequency in the course, obtained either this year or last year;
- The tests average must be greater or equal to 9.5 points; and
- The final grade must be greater or equal to 9.5 points.
Subject matter
1) Modelling state-based concurrent computation with TLA+
2) Specifying a system behaviour with TLA+
3) Exemplifying with representative case studies like: eating philosophers, bakery algorithm, alternating bit protocol, distributed algorithms (e.g. causal message delivery), concurrent abstract data types, etc.
4) Specifying the desired properties of a system (mutual exclusion, (dead)lock-freedom, progress, etc.)
5) Verifying the correctness of a TLA+ specification
6) Modelling transition-based concurrent computation
7) Specifying a system behaviour with dynamic logics like CTL*, mu-calculus and Spatial Logics
8) Verifying dynamic logics specifications with model checking (via the tools TAPAs and SLMC)