Scalable Verification of Variable and Evolvable Systems (SCAVES)

• Applicant: Professorin Dr.-Ing. Ina Schaefer
• Subject Area: Software Engineering and Programming Languages
• Term: from 2011 to 2016
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 198881861

Modern software systems exists in many different variants and evolve over time in order to meet changing requirements. They tend to outgrow the scope of traditional software product lines (SPLs) resulting in ultra-large scale systems (ULSSs) with many interconnected subsystem versions and variants. Multi software product lines (MSPLs) are a special form of ULSS consisting of a composition of several SPLs. Despite their complexity and size, these systems need to satisfy critical properties, such as business-critical or safety-critical requirements. In order to efficiently guarantee these properties, we need scalable verification techniques. In the second phase of the SCAVES project, we aim at extending the scalable modeling, specification and deductive verification techniques, which we have developed for evolving SPLs, to ultra-large scale systems in form of MSPLs. We provide abstract modeling concepts for the problem space, the solution space and the configuration space of MSPLs and instantiate it to the programming language level. The modeling approach is based on an interface concept between the composed SPLs in order to provide a compositional system structure. To ensure critical system properties, we devise a specification technique which allows us to relativize system properties towards the composed SPLs and use assume-guarantee style reasoning for compositional verification. As MSPLs evolve as any other software system, we incorporate incremental modeling, specification and deductive verification techniques in order to efficiently deal with MSPL evolution.

• DFG Programme: Research Grants