Skalierbare Verifikation von Variablen und Evolvierenden Systemen (SCAVES)

• Antragstellerin: Professorin Dr.-Ing. Ina Schaefer
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2011 bis 2016
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 198881861

Moderne Softwaresysteme existieren in verschiedenen Varianten und evolvieren mit der Zeit, um sich verändernden Anforderungen anzupassen.Sie tendieren dazu, den bisherigen Umfang von Software Produktlinien (SPLs) zu überschreiten, und bilden Ultra-large Scale Systems (ULSSs) mit vielen kommunizierenden Subsystemversionen und -varianten. Multi Software Produktlinien (MSPLs) sind eine Spezialform von ULSSs und bestehen aus einer Komposition von mehreren SPLs. Trotz ihrer Komplexität und Größe ist es notwendig, dass diese Systeme kritische Eigenschaften, z.B. geschäftskritische oder sicherheitskritische Anforderungen, erfüllen. Um die Eigenschaften effizient garantieren zu können, bedarf es einer skalierbaren Verifikationstechnik.In der zweiten Phase des SCAVES Projekts werden wir die skalierbaren Modellierungs-, Spezifikations- und deduktive Verifikationstechniken, welche wir für evolvierende SPLs entwickelt haben, auf ULSSs in Form von MSPLs erweitern. Wir stellen abstrakte Modellierungskonzepte für den Problemraum, den Lösungsraum und den Konfigurationsraum von MSPLs bereit und instanziieren diese auf der Programmiersprachenebene. Der Modellierungsansatz basiert auf einem Interfacekonzept zwischen den komponierten SPLs, um eine kompositionale Systemstruktur zu ermöglichen. Um kritische Systemeigenschaften sicherzustellen, entwickeln wir eine Spezifikationstechnik, welche globale Systemeigenschaften auf Eigenschaften der komponierten SPLs herunterbricht, und zeigen diese durch eine kompositionale Verifikationstechnik, die an das "Assume-Guarantee Reasoning" angelehnt ist. Da MSPLs wie andere Softwaresysteme evolvieren, verwenden wir außerdem inkrementelle Modellierungs-, Spezifikations- und deduktive Verifikationstechniken, um effizient mit evolvierenden MSPLs umgehen zu können.

• DFG-Verfahren: Sachbeihilfen