Stud.IP Uni Oldenburg
University of Oldenburg
22.11.2019 02:52:47
inf205 - Formal Methods in Embedded System Design (Complete module description)
Original version English Download as PDF
Module label Formal Methods in Embedded System Design
Module code inf205
Credit points 6.0 KP
Workload 180 h
Faculty/Institute Department of Computing Science
Used in course of study
  • Bachelor's Programme Computing Science (Bachelor) >
  • Dual-Subject Bachelor's Programme Computing Science (Bachelor) >
  • Master of Education Programme (Gymnasium) Computing Science (Master of Education) >
Contact person
Module responsibility
Authorized examiners
Entry requirements
Skills to be acquired in this module
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:
Module contents
The module explains semantic models for reactive, real-time, and hybrid discrete-continuous systems and gives examples for pertinent specification logics. It gradually develops state-exploratory verification algorithms, both of explicit-state and symbolic shape, as relevant to the development of reliable hardware and software systems.

The lectures present the semantic, logical, and algorithmic foundations of the automatic analysis for embedded software systems. The exrcise classes complement this by providing space for experimenting with formalisms and tools in teams. The second half of the semester is dedicated to the semester project, which either deals with implementing an automatic verifier or with in-depth usage of existing tools on examples of indsutrially relevant size
Reader's advisory
  • 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
Language of instruction German
Duration (semesters) 1 Semester
Module frequency jährlich
Module capacity unlimited
Modullevel AS (Akzentsetzung / Accentuation)
Modulart je nach Studiengang Pflicht oder Wahlpflicht
Lern-/Lehrform / Type of program V+Ü
Vorkenntnisse / Previous knowledge Fundierte Grundkenntnisse in mathematischer Logik, diskreter Mathematik, Automaten- und Berechenbarkeitstheorie, wie sie in den Modulen "Diskrete Strukturen" und "Theoretische Informatik I + II" vermittelt werden. Zudem Programmierkenntnisse, wie sie im "Programmierkurs" erworben werden.

Begründung: Die in der Vorlesung vorgestellten Verfahren basieren auf einer Operationalisierung von Semantik durch Reduktion auf logische Kodierungen und mechanisierte Prüfung logischer Aussagen. Ein Verständnis dieser Inhalte sowie ihre werkzeugtechnische Umsetzung bedarf der Grundlagen aus den vorgenannten Veranstaltungen.
Course type Comment SWS Frequency Workload attendance
Lecture 3.00 WiSe 42 h
Exercises 1.00 WiSe 14 h
Total time of attendance for the module 56 h
Examination Time of examination Type of examination
Final exam of module
at the end of the semester
Semester project