CloseHelpPrint
Kies de Nederlandse taal
Course module: 2IWA0
2IWA0
Automotive software engineering
Course info
Course module2IWA0
Credits (ECTS)5
Category3 (Advanced)
Course typeBachelor College
Language of instructionEnglish
Offered byEindhoven University of Technology; Mathematics and Computer Science; Computer Science;
Is part of
Automotive
Contact personprof.dr.ir. J.F. Groote
Telephone5003
E-mailj.f.groote@tue.nl
Lecturer(s)
Responsible lecturer
prof.dr.ir. J.F. Groote
Feedback and reachability
Other course modules lecturer
Contactperson for the course
prof.dr.ir. J.F. Groote
Other course modules lecturer
Academic year2017
Period
2  (13/11/2017 to 04/02/2018)
Starting block
2
TimeslotB: B - Mo 5-8, Tu 9-10, We 1-4
Course mode
Fulltime
Remarks-
Registration openfrom 15/06/2017 up to and including 15/10/2017
Application procedureYou apply via OSIRIS Student
Explanation-
Registration using OSIRISYes
Registration open for students from other department(s)Yes
Pre-registrationNo
Waiting listNo
Number of insufficient tests-
Number of groups of preference0
Learning objectives
The 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 Hennessy-Milner 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

Content
Viewing 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.
Hennessy-Milner logic with fixed point operators and data.
Linearisation of processes.
Confluence and tau-prioritisation.




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 requirements
The following course modules must be completed:
- Computation for automotive (5AIA0)
- Vehicle networking (5AIC0)
Entrance requirements tests
-
Assumed previous knowledge
-
Previous knowledge can be gained by
-
Resources for self study
-
Short promotional description of the course
-
Short promotional description of the course
-
Bachelor College or Graduate School
Bachelor College
URL study guide
http://www.win.tue.nl/~jfg/educ/educ.html
URL study guide
http://www.win.tue.nl/~jfg/educ/educ.html
Required materials
J.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 materials
-
Instructional modes
Guided selfstudy

General
-

Remark
-
Lecture

General
-

Remark
-
Tests
Assignment
Test weight50
Minimum grade-
Test type-
Number of opportunities1
OpportunitiesBlock 2
Test duration in minutes-

Assessment
-

Remark
-

Written examination
Test weight50
Minimum grade5
Test typeFinal examination
Number of opportunities2
OpportunitiesBlock 2, Block 3
Test duration in minutes180

Assessment
-

Remark
-

CloseHelpPrint
Kies de Nederlandse taal