Semester: winter 2020/21
Lectures: Mon 15:40, online (Pavel Parízek, Martin Nečaský)
Labs: Wed 9:00, online
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.2020 Organization & Introduction to Formal Methods lecture00.pdf
12.10.2020 Algebraic Specification Methods and Languages lecture01.pdf
19.10.2020 Rewriting Systems lecture02.pdfmaude-examples.zip
2.11.2020 Model-Oriented Specifications & Language Z lecture03.pdfSyntax of ZBank account
9.11.2020 Advanced Usage of Z: Objects & Refinement lecture04.pdfSyntax of Object-ZRefinement
16.11.2020 Model-Based Specification in VDM lecture05.pdfPublic Transport SystemVDM reference
23.11.2020 Alloy: Language & Tool lecture06.pdfFactoryFactory-dynamicAlloy reference

Labs

Date Topic Examples
14.10.2020 Algebraic Specification Methods  
21.10.2020 Executable Specifications Using Maude Maude programs
4.11.2020 Model-Oriented Specifications with Z File system
11.11.2020 Realistic Case Study  
18.11.2020 Tools for VDM  
25.11.2020 Practical Experience with Alloy  

Homework Assignments

Topic Deadline
Maude: card payment terminal 23.11.2020
VDM or Alloy: smart home 31.12.2020