Am 1. April 2017 hat das i11-Forschungsprojekt zu formaler Spezifikation und Analyse von Anforderungen an Steuerungssoftware begonnen. Es wird während seiner dreijährigen Laufzeit von der DFG gefördert.

Dieses Projekt hat zum Ziel, Anforderungen bereits in der Entwurfsphase auf Korrektheit und Widerspruchsfreiheit zu untersuchen, ohne auf eine Implementierung angewiesen zu sein.

Unser Lösungsansatz beruht auf bedingten Spezifikationen („conditionals“), bei denen eine Anforderung als Paar aus Vorbedingung und Nachbedingung formuliert wird.

Bei der anschließenden Modellprüfung suchen wir nach Inkonsistenzen zwischen Anforderungen auf Systemebene und ihrer Zerlegung in Komponentenanforderungen.

Um die Suche zu beschleunigen, setzen wir Verfahren der gerichteten Modellprüfung („directed model checking“) ein, die auf heuristischer Suche beruhen.

Für die notwendigen Abstandsschätzungen zum Ziel- bzw. Fehlerzustand testen wir neue Maße auf Grundlage von Klassifikationstheorie und statistischem Lernen.