Semester: winter 2025/26
Lectures: Thu 14:00, S4 (Pavel Parízek)
Labs: Thu 15:40, S4
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
2.10.2025 Organization & Introduction to Formal Methods lecture00.pdf
16.10.2025 Algebraic Specification Methods and Languages lecture01.pdf, Examples
23.10.2025 Rewriting Systems lecture02.pdf, maude-examples.zip
30.10.2025 State-Based Modeling Languages & Z Notation lecture03.pdf, Syntax of Z, Bank account
6.11.2025 State-Based Methods: Refinement & Model-Based Testing lecture04a.pdf, Syntax of Object-Z, Refinement
6.11.2025 Automated Reasoning lecture04b.pdf
13.11.2025 Model-Based Specification in VDM lecture05.pdf, Public Transport System, Student IS - Tests, VDM reference
20.11.2025 Alloy: Language & Tool lecture06.pdf, Factory, Factory-dynamic, Alloy reference, Example - operations
27.11.2025 UML: Unified Modeling Language lecture07a.pdf
27.11.2025 OCL: Object Constraint Language lecture07b.pdf

Labs

Date Topic Examples
16.10.2025 Algebraic Specification Methods Stack, List, ATM
23.10.2025 Executable Specifications Using Maude Maude programs
30.10.2025 State-Based Models and Specifications with Z File system
6.11.2025 Realistic Case Studies: Modeling, Verification  
13.11.2025 Tools for VDM Elections
20.11.2025 Practical Experience with Alloy  
27.11.2025 UML & OCL: Practice  

Homework Assignments

Topic Deadline
Maude: Autonomous Car 20.11.2025
VDM or Alloy: automated smart warehouse 31.12.2025
UML and OCL: management of public Zoo 11.1.2026

Archive

Academic year 2021/2022: lectures examples