Directed Studies: Systems Specification Using TLA+

Schedule:

  • Course (Prof. Dr. Stefan Leue)
    Tuesday      13:30 - 15:00         Room PZ 901         Start: 24 October 2023
  • Tutorial (Raffael Senn)
    Wednesday 10:00 - 11:30         Room PZ 901         Start: 8 November 2023

Description:

Workload

180 hours, of which 56 hours are spent in class and 96 hours of self study.

Prerequesites

Willingness to work with a formal logic and concepts from discrete mathematics, and to accept that software is more than code.

Contents

Software is more than just code. Before we write code, we want to fully and precisely understand what it is supposed to accomplish.  The mere reflection of what a piece of software is supposed to do is likely to lead to correct and more robust code.

Against this backdrop, Turing-Award winner and Microsoft researcher Leslie Lamport has developed the TLA+ logic that allows for precisely specifying the desired capabilities of a software (or hardware) module and its internal and external interfaces. The formal, logic-based capture of these desired capabilities is referred to as a specification. As an example, consider the property that if a module invokes another module, it needs to receive a reply within 50 ms, which can be formally specified in TLA+.  In order to check a TLA+ specification for various types of properties, a range of tools has been developed, including the TLC model checker. The application of TLA+ in the development cycle contributes to rigorous requirements engineering and analysis, thereby supporting software quality. TLA+ is being used in industry, for instance at Amazon, Intel and Microsoft (see https://lamport.azurewebsites.net/tla/industrial-use.html).

Teaching methods

Directed studies course (flipped classroom).

Learning objectives

This course has two main objectives: 

  1. Participants will be enabled to apply formal software engineering methods effectively to their own software development projects.
  2. Participants will learn to acquire scientific material from a textbook and to present this to an audience (in this sense it is also very suitable for teachers students / Lehramtstudierende).

Course literature

Leslie Lamport, Specifying Systems, Addison-Wesley, 2002. Available from https://lamport.azurewebsites.net/tla/book.html.

Record of academic assessments

Presentation of at least one reading assignment. Final examination (most likely oral).

Target group

Master-level and advanced Bachelor students.

Expected course achievment

Presentation of at least one reading assignment. Final examination (most likely oral).

Mandatory requirement

Basic programming, algorithms and systems knowledge. Discrete Mathematics, in particular an introduction into formal logic.

Credits

ECTS-points: 6

Weekly teaching hours

SWS: 2