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.