CPS – Modelling and verification course
April 4 – April 7, 2017
Institute for Real-Time Computer Systems
Room 4981
Technical University of Munich
Arcisstr. 21
Munich, Bayern 80290 Germany
(walking distance from Theresienstraße U-Bahn stop)

Google map

The course involves lectures and exercises (including programming exercises) to be done by the participants.

Course schedule:
Tuesday, 4 April, 2017
———————-
10:00 – 11:30
Introduction to model checking (Samarjit Chakraborty, TUM)

11:30 – 13:00
Lunch

13:00 – 14:30
Formal specification using the synchronous language Esterel (Samarjit Chakraborty, TUM)

14:30 – 15:30
Coffee break

15:30 – 17:00
Semantics of Esterel (Samarjit Chakraborty, TUM)

Wednesday, 5 April, 2017
————————
10:00 – 11:30
Lab session I: Model checking Esterel specifications (Martin Becker, TUM)

11:30 – 13:00
Lunch

13:00 – 14:30
Lab session II: Model checking Esterel specifications (Martin Becker, TUM)

14:30 – 15:30
Coffee break

15:30 – 17:00
Lab session III: Model checking Esterel specifications (Martin Becker, TUM)

Thursday, 6 April, 2017
———————–
10:00 – 11:30
Introduction and applications of temporal logic – LTL, CTL (Lei Feng, KTH)

11:30 – 13:00
Lunch

13:00 – 14:30
Spin model-checker and Simulink design verifier crash course, principles and tool implementations  (Lei Feng, KTH)

14:30 – 15:30
Coffee break

15:30 – 17:00
CPS development perspectives I
– what kind of models are involved in CPS development?
– what is a model? what are relevant model characteristics?
– why modeling? When to model, modeling pitfalls and trade-offs
(Martin Törngren, KTH)

Friday, 7 April, 2017
———————
10:00 – 11:30
Spin model-checker and Simulink design verifier crash course, principles and tool implementations – exercises (Lei Feng, KTH)

11:30 – 13:00
Lunch

13:00 – 14:30
CPS development perspectives II
– trends, challenges and opportunities in the broader CPS MBSE landscape
– selected industrial best practices including MIL, SIL, PIL, HIL and VIL
– contracts to structure and formalize requirements
– model and tool integration: modeling hubs, model exchange, linked data, co-simulation
(Martin Törngren, KTH)

14:30 – 15:30
Coffee break

15:30 – 17:00
Common discussion and wrap-up
– summary of the week – topics taught
– discussion involving the ESRs, reflecting on how the taught topics relate to their research
– Suggestion that each ESR writes down reflections and then that there is a discussion
– panel discussion among teachers: trends, challenges and opportunities for CPS modeling and verification
(All lecturers)