Semester: winter 2021/22
Lectures: Tue 10:40, S11 (Pavel Parízek, Martin Nečaský)
Labs: Tue 12:20, S11
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.


Date Title Downloads
5.10.2021 Organization & Introduction to Formal Methods lecture00.pdf
12.10.2021 Algebraic Specification Methods and Languages lecture01.pdf
19.10.2021 Rewriting Systems
26.10.2021 Model-Oriented Specifications & Language Z lecture03.pdfSyntax of ZBank account
2.11.2021 Advanced Usage of Z: Objects & Refinement lecture04.pdfSyntax of Object-ZRefinement
9.11.2021 Model-Based Specification in VDM lecture05.pdfPublic Transport SystemVDM reference
16.11.2021 Alloy: Language & Tool lecture06.pdfFactoryFactory-dynamicAlloy reference
23.11.2021 UML: Introduction & Class Diagrams UML_Introduction.pdfUML_Class_Diagrams_01.pdfUML_Class_Diagrams_02.pdf
7.12.2021 Object Constraint Language OCL_01.pdfOCL_02.pdf
14.12.2021 Petri Nets lecture09.pdf
4.1.2022 Temporal Logics lecture10.pdf
4.1.2022 Automated Reasoning & Runtime Verification lecture11.pdf
4.1.2022 Summary summary.pdf


Date Topic Examples
12.10.2021 Algebraic Specification Methods  
19.10.2021 Executable Specifications Using Maude Maude programs
26.10.2021 Model-Oriented Specifications with Z File system
2.11.2021 Realistic Case Study  
9.11.2021 Tools for VDM  
16.11.2021 Practical Experience with Alloy  
14.12.2021 Petri Nets: Tools & Examples  

Homework Assignments

Topic Deadline
Maude: ATM 16.11.2021
VDM or Alloy: smart home 31.12.2021
UML and OCL  
Colored Petri Nets or TLA+/PlusCal: online shop 13.2.2022