Scalable Verification of Variable and Evolvable Systems (SCAVES)

点击翻译按钮获取中文摘要

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.