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

• Erstellungsjahr: 2015

Zusammenfassung der Projektergebnisse

Modern software systems are getting more and more complex. They exist in many different variants at one point in time to adapt to their application context. Furthermore, software system evolve over time in order to react to changing environment conditions and user requirements. A software product line is a set of systems with well-defined variabilities and commonalities which are captured by problem space variability models, such as feature models, and variable solution space artefacts that are reused to build the product variants. For safety-critical, business-critical or mission-critical systems, it is essential to guarantee quality and trustworthiness of these system variants and their versions. The overall goal of the SCAVES projects was to develop scalable verification techniques for deductively verifying properties of variable and evolvable system implementations on the source code level. Scalable verification techniques need appropriate modelling and specification techniques as a foundation. Hence, the first key result of the SCAVES projects is delta modelling for capturing spatial and temporal variability of software product lines on the solution space level. Delta modelling is a modular modelling approach for variable and evolvable systems that is language-independent and allows capturing system variability and evolution by the same means. Deltas are a container of changes to a model or a program which can be anticipated in the sense of variability or unanticipated in the sense of evolution. A program/model variant is derived by applying a set of deltas in a suitable order to the empty model/program. In order to specify properties of delta-oriented software product lines, we base our work on contractbased specifications and use delta-operations also on the specification level. Additionally, we specify deltas with assumptions and guarantees towards variable system parts. The second key result of the SCAVES projects is a taxonomy of software product line analysis strategies. Product-based verification considers each product in isolation. The advantage is that verification techniques and tools do not have to be adapted and can be used off-the-shelf. However, the shared software parts are verified repeatedly. In order to obtain more efficient verification, family-based approaches consider a meta-representation of all possible program variants and verify it in one analysis run. This reduces redundant analysis steps. But, the meta-representation assumes a closed variant space which makes it difficult to deal with unanticipated evolution. Delta-based verification approaches consider only the building blocks of the product variants, in our case, the deltas, and verify each building block in isolation. However, as most properties are not compositional, delta-based verification strategies cannot be applied separately. Instead, they have to be combined with either a family-based or a product-based verification step. This results in combined verification strategies, i.e., delta-family-based and delta-product-based analyses. In the SCAVES projects, we have developed exemplary deductive verification approaches for the described product line analysis strategies leading to scalable verification techniques for variable and evolvable system implementations.

Projektbezogene Publikationen (Auswahl)

• Family-based deductive verification of software product lines. GPCE 2012: 11-20
  Thomas Thüm, Ina Schaefer, Martin Hentschel, Sven Apel
  
• Reuse in Software Verification by Abstract Method Calls. CADE 2013: 300-314
  Reiner Hähnle, Ina Schaefer, Richard Bubel
  
• A Classification and Survey of Analysis Strategies for Software Product Lines. ACM Comput. Surv. 47(1): 6:1-6:45 (2014)
  Thomas Thüm, Sven Apel, Christian Kästner, Ina Schaefer, Gunter Saake
  
• Verifying traits: an incremental proof system for fine-grained reuse. Formal Asp. Comput. 26(4): 761-793 (2014)
  Ferruccio Damiani, Johan Dovland, Einar Broch Johnsen, Ina Schaefer
  
• Abstract delta modelling. Mathematical Structures in Computer Science 25(3): 482-527 (2015)
  Dave Clarke, Michiel Helvensteijn, Ina Schaefer
  
• Variability encoding: From compile-time to load-time variability. J. Log. Algebr. Meth. Program. 85(1): 125-145 (2016)
  Alexander von Rhein, Thomas Thüm, Ina Schaefer, Jörg Liebig, Sven Apel