inf205 - Formal Methods in Embedded System Design (Complete module description)

inf205 - Formal Methods in Embedded System Design (Complete module description)

Original version English PDF Download
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
  • Bachelor's Programme Computing Science (Bachelor) >
  • Dual-Subject Bachelor's Programme Computing Science (Bachelor) >
  • Master of Education Programme (Gymnasium) Computing Science (Master of Education) >
Zuständige Personen
  • Fränzle, Martin Georg (module responsibility)
  • Lehrenden, Die im Modul (Prüfungsberechtigt)
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:
  • 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
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 verification

tools, 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
  • Michael Huth, Mark Ryan: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, 2004.
  • Christel Baier, Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008.
  • Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model Checking. MIT Press, 2000.
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.
Form of instruction 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
  • 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
Semester project