Specification and automated validation of staged reconfiguration processes for dynamic software product lines
详细信息 查看全文
- 作者：Malte Lochau ; Johannes Bürdek ; Stefan Hölzle ; Andy Schürr
- 关键词：Dynamic software product lines ; Staged configuration ; Model ; based domain engineering and validation ; Model checking
- 刊名：Software & Systems Modeling
- 出版年：2017
- 出版时间：February 2017
- 年：2017
- 卷：16
- 期：1
- 页码：125-152
- 全文大小：
- 刊物类别：Computer Science
- 刊物主题：Software Engineering/Programming and Operating Systems; Programming Techniques; Software Engineering; Programming Languages, Compilers, Interpreters; Information Systems Applications (incl.Internet);
- 出版者：Springer Berlin Heidelberg
- ISSN：1619-1374
- 卷排序：16
文摘
Dynamic software product lines (DSPLs) propose elaborated design and implementation principles for engineering highly configurable runtime-adaptive systems in a sustainable and feature-oriented way. For this, DSPLs add to classical software product lines (SPL) the notions of (1) staged (pre-)configurations with dedicated binding times for each individual feature, and (2) continuous runtime reconfigurations of dynamic features throughout the entire product life cycle. Especially in the context of safety- and mission-critical systems, the design of reliable DSPLs requires capabilities for accurately specifying and validating arbitrary complex constraints among configuration parameters and/or respective reconfiguration options. Compared to classical SPL domain analysis which is usually based on Boolean constraint solving, DSPL validation, therefore, further requires capabilities for checking temporal properties of reconfiguration processes. In this article, we present a comprehensive approach for modeling and automatically verifying essential validity properties of staged reconfiguration processes with complex binding time constraints during DSPL domain engineering. The novel modeling concepts introduced are motivated by (re-)configuration constraints apparent in a real-world industrial case study from the automation engineering domain, which are not properly expressible and analyzable using state-of-the-art SPL domain modeling approaches. We present a prototypical tool implementation based on the model checker SPIN and present evaluation results obtained from our industrial case study, demonstrating the applicability of the approach.