Home
People
Research
Seminar
Software
Publications
For Students
Links
ContactFormal Foundations of Software Engineering
| Semester | winter 2018/2019 |
|---|---|
| Lecturers | Martin Nečaský Pavel Parízek |
| Time and Location |
lecture: Fri 9:00 S9
lab: Fri 10:40 S9 |
| Information in SIS | NTIN043 |
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 | Topic | Examples |
|---|---|---|
| 5.10.2018 | Organization & Introduction to Formal Methods | |
| 12.10.2018 | Algebraic Specification Methods and Languages | |
| 19.10.2018 | Rewriting Systems | Maude examples |
| 26.10.2018 | Model-Oriented Specifications & Language Z | Syntax of Z | Bank account |
| 9.11.2018 | Advanced Usage of Z: Objects & Refinement | Syntax of Object-Z | Refinement |
| 16.11.2018 | Model-Based Specification in VDM | Public Transport System | VDM reference |
| 23.11.2018 | Alloy: Language & Tool | Factory (dynamic) | Alloy reference |
| 30.11.2018 | UML: Introduction & Class Diagrams (part 1, part 2) | |
| 14.12.2018 | Object Constraint Language (part 1, part 2) | |
| 4.1.2019 | Petri Nets | |
| 11.1.2019 | Temporal Logics | Summary |
Labs
| Date | Topic | Examples |
|---|---|---|
| 12.10.2018 | Algebraic Specification Methods | |
| 19.10.2018 | Executable Specifications Using Maude | Maude programs |
| 26.10.2018 | Model-Oriented Specifications with Z | File system |
| 9.11.2018 | Realistic Case Study | |
| 16.11.2018 | Tools for VDM | |
| 23.11.2018 | Practical Experience with Alloy | |
| 4.1.2019 | Petri Nets: Tools & Examples |
Homework Assignments
| Topic | Deadline |
|---|---|
| Maude: ATM | 23.11.2018 |
| VDM or Alloy: smart home | 31.12.2018 |
| UML and OCL | |
| Colored Petri Nets or TLA+/PlusCal: online shopping | 15.2.2019 |
