inf205  Formal Methods in Embedded System Design (Complete module description)
Module label  Formal Methods in Embedded System Design 
Modulkürzel  inf205 
Credit points  6.0 KP 
Workload  180 h 
Institute directory  Department of Computing Science 
Verwendbarkeit des Moduls 

Zuständige Personen 

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 tooltechnical implementation requires the basics from the aforementioned courses. 
Skills to be acquired in this module  The module provides an overview over semantic models for reactive systems, realtime systems ,and hybrid systems, as well as examples of corresponding specification logics. It explains stateexploratory 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:
Methological competences The students:
The students:
The Students:

Module contents  Embedded computer systems maintain constant interaction with their environment. This induces interaction sequences that are difficult to predict, which complicates the construction and validation of such systems. Akin to the use of structural models for rigorous validation of building layouts in the construction industry, formal models in computer science have consequently been developed for analysis of various aspects of computing systems in general and embedded systems in particular. They cover execution time, energy demand, or possible system dynamics of embedded systems. They represent the respective aspect of the system in a closed form and thus allow for the  often fully automatic  derivation of reliable certificates that apply to any interaction scenario with the environment. This is in contrast to methods of testing or profiling, which only test selected scenarios and thus can only provide limited coverage. In this module, various such models are explained and methods for their fully automatic analysis i.e., derivation certificates or synthesis i.e., automatic generation of correct system designs from such models are explained and demonstrated in their application. The exercises provide opportunity for deepening understanding through handson experience with domainspecific modelling and verificationtools, as well as by creating a (small) fully automated verification tool yourself in a guided process. In the lectures, the semantic, logical, and algorithmic basics of automatic analysis of embedded software systems are taught. The primary form of instruction is the mediasupported lecture as well as the didactic questionanswer game,. In the exercise classes, the knowledge acquired in the lecture is deepened and put into practice. For this purpose, in the first half of the semester, exercises are set fortnightly, the completion of which in small groups encourages independent testing of the individual understanding of the topic and peer teaching. In the second half of the semester, a larger tool development task is set, also to be pursued on in small groups of 3 students each. The work on these projects spans the entire second half of the semester and offers the possibility of projectoriented learning. In this phase, the exercise classes serve as consultation time with the lecturers; in particular, solution approaches and problems can be presented and discussed. 
Literaturempfehlungen 

Links  
Languages of instruction  German, English 
Duration (semesters)  1 Semester 
Module frequency  annual 
Module capacity  unlimited 
Teaching/Learning method  V+Ü 
Previous knowledge  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 tooltechnical implementation requires the basics from the aforementioned courses. 
Lehrveranstaltungsform  Comment  SWS  Frequency  Workload of compulsory attendance 

Lecture  3  WiSe  42  
Exercises  1  WiSe  14  
Präsenzzeit Modul insgesamt  56 h 
Examination  Prüfungszeiten  Type of examination 

Final exam of module 

Semester project 