Scalable Verification of Variable and Evolvable Systems (SCAVES)

现代软件系统存在于许多不同的变体中，并随着时间的推移而发展，以满足不断变化的需求。它们倾向于超出传统软件产品线（SPLs）的范围，从而产生具有许多相互连接的子系统版本和变体的超大规模系统（ulss）。多软件产品线（MSPLs）是由多个SPLs组合而成的一种特殊形式的ULSS。尽管这些系统复杂且规模庞大，但它们需要满足关键属性，例如业务关键型或安全关键型需求。为了有效地保证这些属性，我们需要可扩展的验证技术。在SCAVES项目的第二阶段，我们的目标是扩展可扩展的建模、规范和演绎验证技术，这些技术是我们为发展SPLs而开发的，以MSPLs的形式扩展到超大规模的系统。给出了MSPLs的问题空间、解空间和配置空间的抽象建模概念，并将其实例化到编程语言层面。建模方法基于组合SPLs之间的接口概念，以提供组合系统结构。为了确保关键的系统属性，我们设计了一种规范技术，该技术允许我们将系统属性相对于组合的spc，并使用假设保证风格的推理进行组合验证。随着MSPL像其他软件系统一样发展，我们结合了增量建模、规范和演绎验证技术，以便有效地处理MSPL的发展。

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.