Semester: winter 2024/25
Lectures: Tue 15:40, S5 (Pavel Parízek)
Labs: Tue 17:20, S5
Page in SIS: NTIN043
Grading: Credit and exam
Lectures: Tue 15:40, S5 (Pavel Parízek)
Labs: Tue 17:20, S5
Page in SIS: NTIN043
Grading: Credit and exam
The goal of this course is to provide an overview of methods and tools for the formal specification of requirements, architecture and behavior of software systems. We will show practical examples focusing especially on the design phase and validation.
This course is intended for students enrolled to the Master's programme in computer science.
Lectures
| Date | Title | Downloads |
|---|---|---|
| 1.10.2024 | Organization & Introduction to Formal Methods | lecture00.pdf |
| 8.10.2024 | Algebraic Specification Methods and Languages | lecture01.pdf, Examples |
| 22.10.2024 | Rewriting Systems | lecture02.pdf, maude-examples.zip |
| 29.10.2024 | State-Based Modeling Languages & Z Notation | lecture03.pdf, Syntax of Z, Bank account |
| 12.11.2024 | State-Based Methods: Refinement & Model-Based Testing | lecture04.pdf, Syntax of Object-Z, Refinement |
| 19.11.2024 | Formal Approaches in Mainstream | mainstreamswepl.pdf |
| 19.11.2024 | Model-Based Specification in VDM | lecture05.pdf, Public Transport System, VDM reference |
| 26.11.2024 | Alloy: Language & Tool | lecture06.pdf, Factory, Factory-dynamic, Alloy reference |
| 3.12.2024 | UML: Unified Modeling Language | lecture07a.pdf |
| 3.12.2024 | OCL: Object Constraint Language | lecture07b.pdf |
| 10.12.2024 | Petri Nets | lecture08.pdf |
| 17.12.2024 | Temporal Logics | lecture09.pdf |
| 17.12.2024 | Bonus Topics: Automated Reasoning, Runtime Verification | lecture10.pdf |
| 17.12.2024 | Summary | summary.pdf |
Labs
| Date | Topic | Examples |
|---|---|---|
| 8.10.2024 | Algebraic Specification Methods | Stack, List, ATM |
| 22.10.2024 | Executable Specifications Using Maude | Maude programs |
| 29.10.2024 | State-Based Models and Specifications with Z | File system |
| 12.11.2024 | Realistic Case Study | |
| 19.11.2024 | Tools for VDM | Elections |
| 26.11.2024 | Practical Experience with Alloy | |
| 3.12.2024 | UML & OCL: Practice | |
| 10.12.2024 | Petri Nets: Tools & Examples |
Homework Assignments
| Topic | Deadline |
|---|---|
| Maude: Autonomous Car | 26.11.2024 |
| VDM or Alloy: smart home or automated smart warehouse | 31.12.2024 |
| UML and OCL: grocery store | 12.1.2025 |
| Colored Petri Nets or TLA+/PlusCal: air traffic control | 16.2.2025 |
Archive
| Academic year 2021/2022: lectures examples |