Semester: winter 2019/20
Lectures: Mon 14:00, S6 (Pavel Parízek, Martin Nečaský)
Labs: Mon 15:40, S6
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
7.10.2019 Organization & Introduction to Formal Methods lecture00.pdf
14.10.2019 Algebraic Specification Methods and Languages lecture01.pdf
21.10.2019 Rewriting Systems
4.11.2019 Model-Oriented Specifications & Language Z lecture03.pdfSyntax of ZBank account
11.11.2019 Advanced Usage of Z: Objects & Refinement lecture04.pdfSyntax of Object-ZRefinement
18.11.2019 Model-Based Specification in VDM lecture05.pdfPublic Transport SystemVDM reference
25.11.2019 Alloy: Language & Tool lecture06.pdfFactoryFactory-dynamicAlloy reference
9.12.2019 UML: Introduction & Class Diagrams UML_Introduction.pdfUML_Class_Diagrams_01.pdfUML_Class_Diagrams_02.pdf
16.12.2019 Object Constraint Language OCL_01.pdfOCL_02.pdf
6.1.2020 Petri Nets lecture10.pdf
6.1.2020 Temporal Logics lecture11.pdf
6.1.2020 Summary summary.pdf


Date Topic Examples
14.10.2019 Algebraic Specification Methods  
21.10.2019 Executable Specifications Using Maude Maude programs
4.11.2019 Model-Oriented Specifications with Z File system
11.11.2019 Realistic Case Study  
18.11.2019 Tools for VDM  
25.11.2019 Practical Experience with Alloy  
6.1.2020 Petri Nets: Tools & Examples  

Homework Assignments

Topic Deadline
Maude: card payment terminal 25.11.2019
VDM or Alloy: smart home 31.12.2019
UML and OCL  
Colored Petri Nets or TLA+/PlusCal: online shopping 14.2.2020