权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Scalable Verification of Variable and Evolvable Systems (SCAVES)

可变和可演化系统的可扩展验证 (SCAVES)

基本信息

批准号：
198881861
负责人：
Professorin Dr.-Ing. Ina Schaefer
金额：
--
依托单位：
KASTEL - Institut für Informationssicherheit und Verlässlichkeit
依托单位国家：
德国
项目类别：
Research Grants
财政年份：
2011
资助国家：
德国
起止时间：
2010-12-31 至 2015-12-31
项目状态：
已结题

来源：
https://gepris.dfg.de/gepris/projekt/198881861?language=en
关键词：
Scalable Verification Variable Evolvable Systems

项目摘要

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.

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