Semester: winter 2023/24
Lectures: Fri 10:40, S4 (Pavel Parízek)
Labs: Fri 12:20, 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
6.10.2023 Organization & Introduction to Formal Methods lecture00.pdf
13.10.2023 Algebraic Specification Methods and Languages lecture01.pdf
20.10.2023 Rewriting Systems lecture02.pdfmaude-examples.zip
27.10.2023 Model-Oriented Specifications & Language Z lecture03.pdfSyntax of ZBank account
3.11.2023 Advanced Usage of Z: Objects & Refinement lecture04.pdfSyntax of Object-ZRefinement
10.11.2023 Model-Based Specification in VDM lecture05.pdfPublic Transport SystemVDM reference
24.11.2023 Alloy: Language & Tool lecture06.pdfFactoryFactory-dynamicAlloy reference
1.12.2023 UML: Unified Modeling Language lecture07.pdf
8.12.2023 OCL: Object Constraint Language lecture08.pdf
15.12.2023 Petri Nets lecture09.pdf
5.1.2024 Temporal Logics lecture10.pdf
5.1.2024 Automated Reasoning & Runtime Verification lecture11.pdf
5.1.2024 Summary summary.pdf

Labs

Date Topic Examples
13.10.2023 Algebraic Specification Methods  
20.10.2023 Executable Specifications Using Maude Maude programs
27.10.2023 Model-Oriented Specifications with Z File system
3.11.2023 Realistic Case Study  
10.11.2023 Tools for VDM Elections
24.11.2023 Practical Experience with Alloy  
1.12.2023 UML: Practice  
8.12.2023 OCL: Practice  
15.12.2023 Petri Nets: Tools & Examples  

Homework Assignments

Topic Deadline
Maude: Intensive Care Unit 24.11.2023
VDM or Alloy: smart home or automated smart warehouse 31.12.2023
UML and OCL: grocery store 14.1.2024
Colored Petri Nets or TLA+/PlusCal: air traffic control 18.2.2024

Archive

Academic year 2021/2022: lectures examples