URL study guide
https://tue.osiris-student.nl/onderwijscatalogus/extern/cursus?cursuscode=2IMF30&collegejaar=2026&taal=enDescription
The course explains the use of mCRL2, its axioms, abstract data types, process equivalences, the modal mu-calculus with data, a formal proof system, linear processes, transformation to linear processes, and confluence reduction.Keywords are: Process algebra, interactions, behaviour, axioms, derivations, hiding and internal actions, data-process interaction. Linear processes. Confluence. The mCRL2 toolset. State space explosion. Modal logic and model checking. The theoretical part will be finished by an examination. The practical part consists of the design of a small embedded system which is delivered in the form of a technical report. First the requirements must be written down. Second a design of the system must be made and third the requirements must be proven to hold on the system, where faulty performance of some of the components must be taken into account.
Objectives
The purpose of this course is to learn how formal techniques can be used to increase the quality of software in (communicating) systems. Obtaining an appreciation for precise, concise and abstract formalisms lays the foundation to understand the often more wieldy specification formalisms that are around. Students learn how (1) systems are modelled using automata and abstract process formalisms, (2) correctness requirements are formulated using modal logics (esp. the mu-calculus), and (3) correctness of software and models can be established using formal analysis techniques. The student will have obtained basic experience with the actual design of a communicating system that provenly satisfies a number of behavioural requirements that are a priori formulated on the system.Specific learning outcomes
1. Modelling of discrete systems
The student is capable of modelling discrete system behaviour. He has a good understanding of the underlying theory and semantics (states, transitions, and if applicable process equivalences and axioms). He can apply these formalisms to model real world behaviour and he understands to formalisms well enough to prove simple behaviour equal to each other.
2. Requirement specification
Software requirements, modal logic, model checking.
Students can formulate requirements on models or actual software. They can be formulated in terms of process equivalences using hiding, or in terms of modal logics (esp. the mu-calculus). Students know how to verify the properties and are aware of the pitfalls that verification may entail. They understand that different specification styles exist, and that they may influence the verifiability of the designs.
3. System design
Students are capable of applying the techniques for the design of an embedded controller that provably satisfies a number of formal requirements. Students can write a technically competent report about the design of the system and verification of the requirements.