Formale Methoden für den Entwurf und die Analyse komplexer Systeme

Die Computerwissenschaften beschäftigen sich - ähnlich wie die Mathematik - mit abstrakten Objekten. Während es in der Mathematik um Zahlen, Formen, Zusammenhänge usw. geht, stehen in den Computerwissenschaften Begriffe wie Algorithmus und Information im Mittelpunkt. Die Computerwissenschaften sind aber gleichzeitig eine Ingenieursdisziplin. Ingenieure entwerfen etwas: Computeringenieure entwerfen Hardware und - vor allem - Software. Das Ziel jeder Ingenieursdisziplin ist es, das Entwerfen von einer Kunst, in der das Ergebnis vom Talent des Einzelnen abhängt, zu einer Wissenschaft mit einer fundierten Methodik zu entwickeln. Wenn ein Bauingenieur eine Brücke entwirft, weiß er, welche Berechnungen er durchführen muss. Am Ende hält die Brücke genau jene Bedingungen aus, die kalkuliert worden sind. Aber die Computerwissenschaften sind jünger als die Bauwissenschaften, und die mathematischen Methoden zur Vorberechnung der Eigenschaften von Softwaresystemen sind noch nicht ausgereift. Nach erfolgter Softwareentwicklung muss das Ergebnis erst getestet werden, und Softwarefehler sind dennoch gang und gäbe. Es gibt noch einen anderen fundamentalen Unterschied: Entfernt man bei einer Brücke eine einzelne Niete, so bricht diese - im Fall eines guten Entwurfs - nicht gleich zusammen. Ein kleiner Fehler führt nicht sofort zu einer Katastrophe. Bei Software kann man das schwer ausschließen. Wenn man nur einen einzigen Buchstaben in einem Programmtext ändert, kann das den Absturz des Computers zur Folge haben. Die Ursache liegt darin, dass es sich bei Software um ein sogenanntes diskretes System handelt. Das Ziel der Forschung von Thomas A. Henzinger ist die Entwicklung algorithmischer Methoden, die die Zuverlässigkeit von Software verbessern. Die Methoden beruhen auf formaler Logik und mathematischen Theorien zur Modellierung und Analyse diskreter dynamischer Systeme. Besonders schwierig - und daher auch wissenschaftlich besonders interessant - sind Softwaresysteme, die aus vielen miteinander kommunizierenden Teilen bestehen. Eine weitere Herausforderung stellt sich bei Software, die zur Steuerung von kritischen - oft lebenswichtigen - Prozessen eingesetzt wird, wie dies heute in jedem Kraftfahrzeug und Herzschrittmacher der Fall ist. Thomas A. Henzinger und sein Team haben seit über zehn Jahren grundlegende mathematische Modelle für Prozesssteuerungssoftware erarbeitet. Am IST Austria arbeiten Computerwissenschafter und Biologen interdisziplinär zusammen. Insbesondere wird versucht, mathematische Methoden zur Softwaremodellierung auch dahingehend weiterzuentwickeln, dass sie zur Analyse von Prozessen in lebenden Zellen und Organen eingesetzt werden können. Das ultimative Ziel dieser Forschung ist es, einen vollständigen Organismus in Software abzubilden. Der Wittgenstein-Preis wird es ermöglichen, weitere Schritte in diese Richtung zu setzen.

Formal methods can ensure the safety of hardware and software systems, but they can also be used to predict the behavior of complex systems in other domains, such as engineering, economics, and biology. In this project, we developed the following formal methods for the design and analysis of complex systems: (1) solving bidding games on graphs for the design and analysis of stateful auctions; (2) mining hybrid automaton models from time -series data for the modeling and analysis of mixed discrete-continuous systems; (3) model checking the evolution of gene regulatory networks; (4) stepwise refinement and struct ured verification of asynchronous concurrent programs; (5) learning biologically inspired neural network motifs for resilient and interpretable control applications; (6) identifying cost -precision trade-offs in the approximative monitoring of complex systems; (7) predicting the long-run behavior of probabilistic systems through runtime verification; (8) using abstract interpretation for novelty detection and online supervision of neural networks.