Semester: winter 2022/23
Lectures: Wed 10:40, S1 (Pavel Parízek, Martin Nečaský)
Labs: Wed 12:20, S1
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
5.10.2022 Organization & Introduction to Formal Methods lecture00.pdf
12.10.2022 Algebraic Specification Methods and Languages lecture01.pdf
19.10.2022 Rewriting Systems lecture02.pdf, maude-examples.zip
26.10.2022 Model-Oriented Specifications & Language Z lecture03.pdf, Syntax of Z, Bank account
26.10.2022 Advanced Usage of Z: Objects & Refinement lecture04.pdf, Syntax of Object-Z, Refinement
2.11.2022 Model-Based Specification in VDM lecture05.pdf, Public Transport System, VDM reference
23.11.2022 Alloy: Language & Tool lecture06.pdf, Factory, Factory-dynamic, Alloy reference
30.11.2022 UML: Introduction & Class Diagrams UML_Introduction.pdf, UML_Class_Diagrams_01.pdf, UML_Class_Diagrams_02.pdf
7.12.2022 Object Constraint Language OCL_01.pdf, OCL_02.pdf
14.12.2022 Petri Nets lecture09.pdf
21.12.2022 Temporal Logics lecture10.pdf
21.12.2022 Automated Reasoning & Runtime Verification lecture11.pdf
21.12.2022 Summary summary.pdf

Labs

Date Topic Examples
12.10.2022 Algebraic Specification Methods  
19.10.2022 Executable Specifications Using Maude Maude programs
26.10.2022 Model-Oriented Specifications with Z File system
2.11.2022 Realistic Case Study  
2.11.2022 / 16.11.2022 Tools for VDM Elections
23.11.2022 Practical Experience with Alloy  
14.12.2022 Petri Nets: Tools & Examples  

Homework Assignments

Topic Deadline
Maude: Intensive Care Unit 23.11.2022
VDM or Alloy: smart home or automated smart warehouse 31.12.2022
UML and OCL  
Colored Petri Nets or TLA+/PlusCal: air traffic control 12.2.2023

Archive

Academic year 2021/2022: lectures examples