SPECENG: Specification Engineering für temporale logische Spezifikationen

Im spezifikationsgesteuerter Softwareentwicklung sind formale Spezifikationen entscheidend, da sie als Brücke zwischen informellen Anforderungen und maschinenverständlichen Implementierungen fungieren. Sie gewährleisten Korrektheit in jeder Phase, von der Identifizierung von Inkonsistenzen bei der Anforderungsanalyse bis hin zur Generierung von Testfällen. Spezifikationen helfen bei der Überprüfung von Systemeigenschaften und sogar der Synthese korrekter Implementierungen. Die Erstellung valider Spezifikationen bleibt jedoch eine große Herausforderung und wird oft als Engpass bei der Entwicklung qualitativ hochwertiger, zuverlässiger Softwaresysteme angesehen. In diesem Projekt streben wir einen systematischen Prozess zur Entwicklung linearer temporaler logischer Spezifikationen an, die valide sind und die Intention der Ingenieursteams widerspiegeln. Weiterhin sollten die Spezifikationen von hoher Qualität sein – sowohl in Bezug auf das Verständnis durch Ingenieure als auch hinsichtlich ihrer Effizienz für nachgelagerte Software-Engineering-Werkzeuge wie Programmsynthese- und Verifikation-Tools. Daher entwerfen wir einen Prozess der Spezifikationsentwicklung mit folgenden Beiträgen: (1) Zur Sicherstellung der Validität schaffen wir einen neuartigen, bidirektionalen, interaktiven Prozess von der natürlichen Sprache zu LTL-Formeln und zurück durch die interaktive Nutzung von LLMs und positiven sowie negativen Traces. (2) Für die Qualität entwickeln wir einen neuartigen Refactoringansatz, der Anti-Patterns erkennt und behebt und dadurch zu Spezifikationen führt, die für Ingenieure lesbar und für Verifikations- und Syntheseprozesse effizient nutzbar sind.