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

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.

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

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.

• 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.

• 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