Main Content

Formal Methods in Software Engineering

Formal methods are used for the formal specification and analysis of software systems and as a suitable abstraction level for the description and solution of software engineering problems. Starting with finite automata, we begin with the formal specification of simple systems and analyze them using model-checking techniques. To specify and analyze more realistic systems, we refine the state specification using data structures. Graphs can be used flexibly to specify data structures. Their changes can be defined systematically with graph transformations. On this basis, typical software development activities, such as system design and program testing, can be formally specified and analyzed. In addition, we consider simple program verification. Finally, we devote ourselves to a selected problem of software engineering and jointly develop a specification and analysis technique for this problem.

Qualification goals

After completing this module, students will

  • be able to formalize systems, system properties, and software development activities,
  • know how to automatically analyze and verify system properties,
  • be able to evaluate the strengths and weaknesses of formal methods in software engineering,
  • have practiced scientific ways of working (recognizing, formulating, solving problems, training the ability to abstract), and
  • have practiced oral communication skills by practicing free speech in front of an audience and in discussion.

Organizational

Lecturer: Prof. Taentzer
Lecture and exam dates under module number: LV-12-079-200
Exercise dates under module number: LV-12-079-201
SWS: 4+2, Credit points: 9

Prerequisites: None. Recommended are the competences taught in the modules Theoretical Computer Science, Logic and Software Engineering.

Deliverables: Attainment of at least 50 percent of the points from the exercise problems to be worked on each week and oral presentation of the solution to at least two of the exercise problems. Oral examination or written test.

Additional notes: Current information and announcements about the lecture are generally published in the corresponding Ilias group. You can use the folder Software Engineering in Ilias to navigate from there to the current semester and the group matching the course.

Literature

  • H. Balzert: Textbook of Software Engineering - Software Development, 2nd ed., Spektrum Akademischer Verlag 2000
  • C. Baier, J. Katoen: Principles of Model Checking, MIT Press 2008