 Learning objectivesThe first objective of this course is to understand that behaviour of systems is complex, especially if all conceivable behaviour must be designed beforehand. For this it is important that internal and external behaviour of systems are distinguished and that it becomes a second nature to characterise systems by their external behaviour, and hide the internal behaviour as much as possible.
In order to conquer the complexity of behaviour the student learns how to model it using a dedicated formalism, namely mCRL2. Students are expected to be able to model behaviour with this formalism and perform elementary manipulations with these models, such as hiding of actions, behavioural reduction using (branching) bisimulation and (weak) trace equivalence. They must understand when to apply which reduction method. They must be able to visualise and interpret the resulting labelled transition diagrams.
Using modal formulas (behavioural formulas written in a modal logic) the behavioural models are doublechecked to guarantee that they indeed do what is expected from them. In order to achieve this students must understand HennessyMilner logic with fixed points and data. They must be able to translate real world requirements into this formalism. Understanding of elementary rules of transforming formulas into each other is obligatory as well as knowing how to verify them using the tools on the models
 ContentViewing actions as the way to understand elementary communication. Labelled transition systems as the representation of behaviour. Equivalence on labelled transition systems: (weak) trace equivalence; (branching) bisimulation.
The internal action tau. Hiding. Data types; semantics of data types. Elementary calculation with data types. Process algebra. Alternative, sequential and parallel composition. Deadlock. Processes with data and conditions. Recursive processes. Process algebra axioms. Communication and data transfer. Sum elimination theorem. HennessyMilner logic with fixed point operators and data. Linearisation of processes. Confluence and tauprioritisation.
Furthermore, in the assignment a controller for a simple system must be designed, behavioural requirements must be written down and these requirements must be proven to hold. The assignment must be finished with a complete technical document describing the goal of the project, the external and interla actions, the requirements, both in language and as modal formulas, the behavioural model and the verification of the formulas on the model.  Entrance requirementsThe following course modules must be completed:   Computation for automotive (  5AIA0  ) 
  Vehicle networking (  5AIC0  ) 

 Entrance requirements tests Assumed previous knowledgePrevious knowledge can be gained byResources for self studyShort promotional description of the course 
Short promotional description of the course 
Bachelor College or Graduate School 
  Required materialsJ.F. Groote and M.R. Mousavi. Modelling and analysis of communicating systems  MIT Press 2014. For the toolset with lots of additional information see www.mcrl2.org. 
 Recommended materialsInstructional modesGuided selfstudy General Remark  Lecture General Remark 
 TestsAssignmentTest weight   50 
Minimum grade    
Test type    
Number of opportunities   1 
Opportunities   Block 2 
Test duration in minutes    
Assessment Remark
 Written examinationTest weight   50 
Minimum grade   5 
Test type   Final examination 
Number of opportunities   2 
Opportunities   Block 2, Block 3 
Test duration in minutes   180 
Assessment Remark


 