Concurrent and distributed software is nowadays pervasive to most computing devices. However, it is particularly difficult to design and validate. Concurrency bugs appear frequently and have a substantial impact, as not only they may affect many people, but also may cause a severe financial damage. There is thus a pressing need of using rigorous approaches and tools to specify and verify such systems. Industrial actors like Amazon, Facebook, Google, IBM, Intel, Microsoft, or NASA, just to name a few, are using tools to formally guarantee that (parts of) their software is bug-free.

This course covers basic principles, techniques, and some tools to help on the challenging task of developing concurrent software systems. This involves understanding languages to specify systems and their properties. There are various kind of key properties of concurrent systems; we will focus on basic safety and liveness properties, which are enough to express functional requirements of concurrent and distributed algorithms. As basic frameworks, we will explore behavioural models such as automata and transition systems, and state-based models such as the TLA (Temporal Logic of Actions), an approach developed by Lamport. Properties such as deadlock absence or progress can be expressed using specialised logics and automatically checked on tools like TLA+ using model-checking. The modelling and verification techniques covered in this course are used in the design of high assurance systems, or just in large-scale systems where bugs can affect many users.

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

1) Modelling state-based concurrent computation with TLA+

2) Specifying a system behaviour with TLA+

3) Exemplifying with representative case studies like: eating philosophers, bakeryalgorithm, 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)

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/

Basic knowledge of:
1) Programming
2) First-Order Logics
3) Set Theory