Software-intensive systems take an increasingly critical role in many areas of our lives. For example, today's cars, trains, and airplanes run millions lines of code, industrial manufacturing systems are highly automated, and, moreover, software controls critical applications in businesses-, government-, and healthcare applications. These systems become more and more complex due to their increasingly rich functionality and their concurrent and distributed nature.
To ensure the quality of these software systems, formal development and analysis techniques become increasingly important. The application of formal techniques today, however, is limited by three factors. The first factor (1) is certainly the growing complexity of systems, which often prevents exhaustive automated techniques to be applied. The second factor (2) is that formal analysis tools often operate on simple mathematical models, so that integration with the tools and models used by engineers during the development is a challenge. Third (3), many domains lack the expert knowledge of successfully applying formal development analysis techniques.
The goal of this lecture is to, first (1), introduce the students to formal modeling techniques, such as different forms of automata and formal temporal logics. The second goal (2) is to give the students a detailed knowledge of selected analysis techniques and the involved algorithms. The third goal is to give the students an elementary knowledge of applying formal analysis techniques to solve practical software and systems engineering problems.
The prominent analysis technique covered in this lecture is model checking, which is a technique for automatically proving that a dynamic model of a system satisfies a given specification. This lecture also introduces how formal modeling an analysis techniques are applied in the development process of software and systems. Furthermore, this lecture introduces the basic principles of automatically synthesizing software models that satisfy a given specification. On the side, we may explore selected advanced topics, such as formal techniques for real-time systems.
This lecture combines theoretical concepts with their practical application. In order to achieve the above learning objectives, the lecture will be accompanied by a tutorial. In the tutorial, we discuss small exercises. Mainly, however, the students shall work on small-size "mini projects" where they will, for example, prototypically implement model-checking algorithms or apply model-checking tools to model and analyze example systems.
Students shall work collaboratively on the exercises and projects in groups of three to four people.
This lecture will be held in English. It is offered also to students of the international Master program Internet Technologies and Information Systems (ITIS) for students in Braunschweig, Clausthal, Göttingen, and Hanover.
To accommodate for the students not residing in Hannover, we plan to provide students with video recordings of the lectures.