Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Module INF-88-83-M-6

Compositional Techniques for Synthesis and Verification (Seminar) (M, 4.0 LP)

Module Identification

Module Number Module Name CP (Effort)
INF-88-83-M-6 Compositional Techniques for Synthesis and Verification (Seminar) 4.0 CP (120 h)

Basedata

CP, Effort 4.0 CP = 120 h
Position of the semester 1 Sem. irreg.
Level [6] Master (General)
Language [EN] English
Module Manager
Lecturers
Area of study [INF-MPI] Max-Planck-Institute
Reference course of study [INF-88.79-SG] M.Sc. Computer Science
Livecycle-State [NORM] Active

Notice

Each week we will discuss one topic, based on a representative paper. One participant or the instructor is leading the discussion by giving some general instructional content for the current topic and then presenting the core principles covered in the paper. After this, an open discussion among all participants on the current paper and on the transferability of those insights to other areas is encouraged.

Courses

Type/SWS Course Number Title Choice in
Module-Part
Presence-Time /
Self-Study
SL SL is
required for exa.
PL CP Sem.
2S INF-88-83-K-6
Compositional Techniques for Synthesis and Verification (Seminar)
P 28 h 92 h - - PL1 4.0 irreg.
  • About [INF-88-83-K-6]: Title: "Compositional Techniques for Synthesis and Verification (Seminar)"; Presence-Time: 28 h; Self-Study: 92 h

Examination achievement PL1

  • Form of examination: combination of talk and written elaboration
  • Examination Frequency: Examination only within the course

Evaluation of grades

The grade of the module examination is also the module grade.


Contents

Large scale Cyber Physical Systems (CPS) consist of software, hardware, and physical components interacting in a non-trivial manner. Different parts of these systems are set up using very different design principles, ranging form correct-by-design controllers for physical systems modeled by continuous differential equations, to communication protocols, to code generated by compilers with various characteristics. Due to this intrinsic variability of components and the size of the overall system, synthesis or verification tools cannot be efficiently applied in a monolithic manner to ensure that CPS are safe and work as intended. As a first step towards compositional synthesis and verification techniques for CPS, this seminar investigates existing compositional techniques in relevant sub-domains of CPS analysis and design. We will discuss state-of-the art compositional techniques including for example controller synthesis for continuous-time systems, reactive synthesis over game graphs, or verification of software.

We are flexible to shrink or extend the topics dependent on the interests and the number of the participants of the seminar.

Competencies / intended learning achievements

The objectives of this  seminar are:
  • to investigates existing compositional techniques in relevant sub-domains of the analysis and design of Cyber Physical Systems
  • to give students the practical skills to properly report, review, and reference research articles in the field and to openly discuss their findings.

Literature

Requirements for attendance of the module (informal)

None

Requirements for attendance of the module (formal)

None

References to Module / Module Number [INF-88-83-M-6]

Course of Study Section Choice/Obligation
[INF-88.79-SG] M.Sc. Computer Science [Specialisation] Specialization 1 [WP] Compulsory Elective