نظرة عامة على البرنامج

Program Overview

The university program in question is focused on Cyber-Physical Systems (CPS), specifically the course "Formale Methoden für Cyber-Physical Systems" (Formal Methods for Cyber-Physical Systems).

Course Description

Cyber-Physical Systems (CPS) are systems where software and hardware work together correctly. The methods used in software development, such as testing, static analysis, and formal specification and verification, can also be applied to these systems. However, a model of the physical system behavior is required, which can be simulated. Such physical models are typically described using differential equations as "hybrid systems."

Course Objectives

In this seminar, participants will present and experiment with various approaches or scientific papers and their corresponding tools.

Requirements

The requirements for the course include:

• Independent literature research
• Independent practical experiments with the tools
• Oral presentation (approximately 20 minutes)
• Written elaboration (approximately 8-10 pages in LNCS format)

Recommended Prior Knowledge

Recommended prior knowledge includes:

• Formal specification and verification
• Logic and discrete structures

Important Note

Participants are responsible for adhering to good scientific practice, including correct citation in documents (presentations, texts, and drafts). Violations will result in failure to pass the seminar.

Preliminary Schedule

The preliminary schedule includes:

• April 20: Preliminary discussion
• April 27: Topic assignment and tips for literature research
• May 4: Aspects of good presentation
• May 11: Lightning talks
• May 18: Canceled (Ascension Day)
• May 25: Hints for elaboration
• Presentations (two per date):
  • June 1
  • June 8: Canceled (Corpus Christi)
  • June 15
  • June 22
  • June 29
  • July 6
  • July 13
• September 15: Submission of elaboration

Topic List (Preliminary)

The topic list includes:

Model Checking and Algorithms

• Alur et al., Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, 1993
• Alur et al., The Theory of Timed Automata, 1991
• The Simplex algorithm (independent literature research)
• The Runge-Kutta method (independent literature research)

Verification of Machine Learning

• Krasowski et al., Safe Reinforcement Learning for Urban Driving using Invariably Safe Braking Sets, 2022
• Tran et al., NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems, 2020

Analytical Methods

• Prajna et al., Safety Verification of Hybrid Systems Using Barrier Certificates, 2004
• Quesel et al., How to model and prove hybrid systems with KeYmaera: a tutorial on safety, 2016

Real-time Temporal Logic

• Gressenbuch et al., Predictive Monitoring of Traffic Rules, 2021
• Donzé et al., Robust Satisfaction of Temporal Logic over Real-Valued Signals, 2010

Miscellaneous

• Maierhofer et al., Formalization of Intersection Traffic Rules in Temporal Logic, 2022
• Wilhelm et al., The worst-case execution-time problem - overview of methods and survey of tools, 2008

Department and Lecturer

The course is offered by the Institute of Computer Science, with lecturer Gidon Ernst and assistant Marvin Brieger.

Course Participants and Central Allocation

There are 10 participants out of 12, and the course is allocated as a bachelor's seminar. Instructions for registration are provided, but additional applications are not accepted, and the distribution of seminar places is not influenced.