Embedded computer systems sustain a permanent interaction with their environment. This interaction may lead to hardly predictable stimuli and reponse sequences, which complicates the design and validation of such systems tremendously. As in more mature enigneering disciplines, formal analytical models have been proposed as a remedy. Their role in the design flow is equivalent to the use of structural analysis and material science within, e.g., building statics. Pertinent formal methods for and formal models of embedded systems cover, for instance, execution time, power demand, and possible system dynamics. As they represent relevant aspects of a system in a formal, mathematical way, they often permit automatic anaylsis - i.e., to derive characteristic data - and automatic certificate generation. The distinguishing factor to more traditional forms of analysis like testing and profiling is the exhaustive form of analysis achieved by mathematical methods, which guarantee that the results apply for any environmental interaction. This is in stark contrast to the inherently incomplete coverage provided by test-based methods. The lectures explain a series of increasingly more expressive formal models and the related automatic analysis techniques. The exercise classes complement these theoretical insights by hands-on experience with state of the art formal analysis tools and offer the possibility to build such tools oneself.
**Professional competence** The students:
- Evaluate the consequences of certificates applied by formal methods - Evaluate the suitability of available verification tools for a partial aspect and system class - Use these tools and interpret their results and improve the examined system - Prepare system models for automatic analysis methods and abstract or encode the systems symbolically (or otherwise) accordingly - Design and implement verification algorithms
**Methodological competence** The students:
Are able to model complex and heterogeneous systems by adequate mathematical modelling techniques - Know pertinent mathematical models for system dynamics and are able to transfer them to other problem domains.
**Social competence** The students:
- Develop and implement fundamental verification algorithms in teams
- Discuss the relative merits of alternative algorithms and formalisms
**Self-competence** The students - can assess their technical and methodological understanding - reflect on their problem-solving competence with reference to the procedures and methods presented