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:
- Participants will be enabled to apply formal software engineering methods effectively to their own software development projects.
- 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