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 tool-technical 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, 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:
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 hands-on experience with domain-specific 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 media-supported lecture as well as the didactic question-answer 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 project-oriented 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 tool-technical 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 |