Formal methods of embedded systems: Model-based analysis

Contact

Management

Prof. Dr M. Fränzle
Room: D119/120 (OFFIS)
Phone: +49-441-9722 566

Office

Kathrin Kuper
Room: D121 (OFFIS)
Phone: +49-441-9722 501
Fax: +49-441-9722 502

Formal methods of embedded systems: Model-based analysis

This course will be offered in the winter semester 2025/2026. Registration takes place via the .

Semester: Winter term 2025

2.01.205 Formal Methods in Embedded System design -  


Event date(s) | room

Description

Embedded computer systems are in constant interaction with their environment, which can lead to interaction sequences that are difficult to predict. This circumstance complicates the construction and validation of such systems. Similar to the use of engineering mathematics in civil engineering, formal models have therefore been developed for various aspects - e.g. execution time, energy demand, possible system dynamics - of embedded systems under construction. These models represent the respective aspect of the system in a closed form and thus allow the - often fully automatic - derivation of reliable analysis results and formal certificates that apply to any interaction scenario with the environment. This is in contrast to testing or profiling methods for software and hardware, which only test selected scenarios and can therefore only provide limited coverage.

In this module, various such models are explained and methods for their fully automatic analysis - i.e. derivation of characteristic data or generation of certificates of compliance to requirements - or synthesis - i.e. automatic generation of correct system designs - from such models are explained and demonstrated in their application.

In the exercises, students have the opportunity to deepen their knowledge through hands-on experience with domain-typical modelling and verification tools and to create a (small) fully automated verification tool themselves in an assisted process.

The lecture teaches the semantic, logical and algorithmic fundamentals of the automatic analysis of embedded software systems. The primary form of instruction is the media-supported lecture and the didactic question-and-answer game, with presentations, animations and tool demonstrations serving as supporting media.

In the exercises, the knowledge acquired in the lecture is deepened and put into practice. In the first half of the semester, exercises are set fortnightly for this purpose, the completion of which in small groups encourages students to independently test their understanding of the topic and to learn through peer coaching. The second half of the semester then features a larger semester project, to be pursued in groups.

Lecturers

Tutors

SWS
4

Lehrsprache
deutsch und englisch

Anzahl der freigegebenen Plätze für Gasthörende
1

(Changed: 11 Feb 2026)  |  Kurz-URL:Shortlink: https://uol.de/p60236en
Zum Seitananfang scrollen Scroll to the top of the page

This page contains automatically translated content.