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

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

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

Homework Assignments

Topic Deadline
Maude: Autonomous Car 26.11.2024

Archive

Academic year 2021/2022: lectures examples