inf205 - Formal Methods in Embedded System Design (Course overview)

inf205 - Formal Methods in Embedded System Design (Course overview)

Department of Computing Science 6 KP
Module components Semester courses Winter semester 2024/2025 Examination
Lecture
  • Unlimited access 2.01.205 - Formale Methoden Eingebetteter Systeme Show lecturers
    • Janis Kröger, M. Sc.
    • Prof. Dr. Martin Georg Fränzle
    • Paul Kröger

    Tuesday: 10:00 - 12:00, weekly (from 15/10/24), Location: A04 4-414
    Thursday: 10:00 - 12:00, weekly (from 17/10/24), Location: A04 4-407
    Eingebettete Computersysteme stehen in ständiger Interaktion mit ihrer Umgebung, was zu schwer vorhersehbaren Interaktionssequenzen führen kann. Dieser Umstand erschwert Konstruktion und Validation derartiger Systeme. Vergleichbar dem Einsatz statischer und materialkundlicher Modelle in der Bauwirtschaft sind deshalb formale Modelle für verschiedene Aspekte - z.B. Ausführungszeit, Energiebedarf, mögliche Systemdynamik - eingebetteter Systeme entwickelt worden. Diese stellen den jeweiligen Aspekt des Systems in geschlossener Form dar und erlauben damit die - oft vollautomatische - Herleitung von verlässlichen Kenndaten und Zertifikaten, welche für jedes beliebige Interaktionsszenario mit der Umgebung gelten. Dies steht im Gegensatz zu Methoden des Testens oder Profilings, welche nur ausgewählte Szenarien prüfen und somit nur eine begrenzte Überdeckung bieten können. In diesem Modul werden verschiedene derartige Modelle erklärt und Methoden zur vollautomatischen Analyse - d.h. Herleitung von Kenndaten oder Zertifikaten - oder Synthese - d.h. automatischen Erzeugung korrekter Systementwürfe - aus derartigen Modellen erläutert und in ihrer Anwendung gezeigt. In den Übungen besteht die Möglichkeit, die entsprechenden Kenntnisse durch Hands-on-Erfahrung mit domänentypischen Modellierungs- und Verifikationswerkzeugen zu vertiefen, sowie in einem geführten Prozess ein (kleines) vollautomatisches Verifikationswerkzeug selbst zu erstellen. In der Vorlesung werden die semantischen, logischen und algorithmischen Grundlagen der automatischen Analyse eingebetteter Softwaresysteme vermittelt. Die primäre Unterweisungsform ist hierbei der medial unterstützte Vortrag sowie das didaktische Frage-Antwort-Spiel, wobei als unterstützende Medien Präsentationen, Animationen und Werkzeugvorführungen dienen. In den Übungen wird das in der Vorlesung erworbene Wissen vertieft und praktisch umgesetzt. Hierzu werden in der ersten Semesterhälfte zweiwöchentlich Übungsaufgaben gestellt, deren Bearbeitung in Kleingruppen zur eigenverantwortlichen Prüfung des Themenverständnisses und zum partnerschaftlichen Lernen anhält.
Exercises
  • Unlimited access 2.01.205 - Formale Methoden Eingebetteter Systeme Show lecturers
    • Janis Kröger, M. Sc.
    • Prof. Dr. Martin Georg Fränzle
    • Paul Kröger

    Tuesday: 10:00 - 12:00, weekly (from 15/10/24), Location: A04 4-414
    Thursday: 10:00 - 12:00, weekly (from 17/10/24), Location: A04 4-407
    Eingebettete Computersysteme stehen in ständiger Interaktion mit ihrer Umgebung, was zu schwer vorhersehbaren Interaktionssequenzen führen kann. Dieser Umstand erschwert Konstruktion und Validation derartiger Systeme. Vergleichbar dem Einsatz statischer und materialkundlicher Modelle in der Bauwirtschaft sind deshalb formale Modelle für verschiedene Aspekte - z.B. Ausführungszeit, Energiebedarf, mögliche Systemdynamik - eingebetteter Systeme entwickelt worden. Diese stellen den jeweiligen Aspekt des Systems in geschlossener Form dar und erlauben damit die - oft vollautomatische - Herleitung von verlässlichen Kenndaten und Zertifikaten, welche für jedes beliebige Interaktionsszenario mit der Umgebung gelten. Dies steht im Gegensatz zu Methoden des Testens oder Profilings, welche nur ausgewählte Szenarien prüfen und somit nur eine begrenzte Überdeckung bieten können. In diesem Modul werden verschiedene derartige Modelle erklärt und Methoden zur vollautomatischen Analyse - d.h. Herleitung von Kenndaten oder Zertifikaten - oder Synthese - d.h. automatischen Erzeugung korrekter Systementwürfe - aus derartigen Modellen erläutert und in ihrer Anwendung gezeigt. In den Übungen besteht die Möglichkeit, die entsprechenden Kenntnisse durch Hands-on-Erfahrung mit domänentypischen Modellierungs- und Verifikationswerkzeugen zu vertiefen, sowie in einem geführten Prozess ein (kleines) vollautomatisches Verifikationswerkzeug selbst zu erstellen. In der Vorlesung werden die semantischen, logischen und algorithmischen Grundlagen der automatischen Analyse eingebetteter Softwaresysteme vermittelt. Die primäre Unterweisungsform ist hierbei der medial unterstützte Vortrag sowie das didaktische Frage-Antwort-Spiel, wobei als unterstützende Medien Präsentationen, Animationen und Werkzeugvorführungen dienen. In den Übungen wird das in der Vorlesung erworbene Wissen vertieft und praktisch umgesetzt. Hierzu werden in der ersten Semesterhälfte zweiwöchentlich Übungsaufgaben gestellt, deren Bearbeitung in Kleingruppen zur eigenverantwortlichen Prüfung des Themenverständnisses und zum partnerschaftlichen Lernen anhält.
Notes on the module
Prerequisites

Sound basic knowledge in mathematical logic, discrete mathematics, automata and computability theory as taught in the modules "Discrete Structures" and "Theoretical Computer Science I + II". In addition, programming skills as acquired in the "Programming Course".
Justification:
The methods presented in the lecture are based on an operationalization of semantics by reduction to logical encodings and mechanized testing of logical statements. An understanding of these contents as well as their tool-technical implementation requires the basics from the aforementioned courses.
Prüfungszeiten
  • 1st deadline: Submission of the semester project incl. one week after the end of the lecture period of the lecture period; followed by a colloquium and a final discussion
  • 2nd deadline: Repeat of the submission of the semester project incl. written elaboration two weeks before the beginning of the following semester followed by colloquium and final discussion
Module examination

Semester project
Skills to be acquired in this module

The module provides an overview over semantic models for reactive systems, real-time systems ,and hybrid systems, as well as examples of corresponding specification logics. It explains state-exploratory verification procedures in both explicit and symbolic variants. The knowledge acquired can be employed in all domains requiring the development of reliable software and hardware systems is concerned
Professional competences
The students:

  • make a sound judgement on the scope of the certificates that can be obtained with formal methods
  • assess the suitability of available verification tools for a particular problem and system class
  • use automatic analysis tools on real systems, interpret the results obtained and subsequently improve the system under investigation in an informed and targeted manner
  • prepare system models for automatic analysis procedures and encode them symbolically (or otherwise)
  • design and implement their own verification algorithms


Methological competences

The students:

  • master the mathematical modelling of complex and heterogeneous dynamical systems
  • know relevant mathematical models of dynamic systems and can instantiate them to new problem classes

Social competences
The students:

  • together in a team develop and implement basic algorithms of automatic verification
  • discuss the advantages and disadvantages of algorithmic alternatives and different formalisations

Self competences

The Students:

  • can assess their technical and methodological understanding
  • reflect on their problem-solving competence with reference to the procedures and methods presented