ProFeat: feature-oriented engineering for family-based probabilistic model checking
ProFeat: feature-oriented engineering for family-based probabilistic model checking
复制标题
DOI：
10.1007/s00165-017-0432-4
复制
发表时间：
2018-01-01
影响因子：
1
通讯作者：
Baier, Christel
中科院分区：
文献类型：
--
作者：
Chrszon, Philipp;Dubslaff, Clemens;Baier, Christel
特性的概念为指定系统族提供了一种精妙的方法。给定一个基础系统，特性封装了额外的功能，这些功能可以被激活或停用，以增强或限制基础系统的行为。特性还可以通过利用族成员的共性并进行一体化分析来促进系统族的分析，在一体化分析中，族中的所有系统在一个单一的族模型上一次性进行分析，而不是逐个分析。最为突出的是，特性的概念已成功应用于描述和分析（软件）产品线。我们介绍工具ProFeat，它通过概率模型检验支持随机系统的面向特性的工程过程。为了描述随机系统族，ProFeat通过面向特性的概念扩展了著名的概率模型检验器Prism的模型，包括对具有动态特性切换、多特性和特性属性的概率产品线的支持。ProFeat为Prism得到的每个族成员的分析结果提供了一种紧凑的符号表示，以支持例如在面向特性的开发过程中的模型修复或细化。通过几个案例研究，我们展示了ProFeat如何简化基于族的定量分析，并比较了逐个分析和一体化分析方法。
The concept of features provides an elegant way to specify families of systems. Given a base system, features encapsulate additional functionalities that can be activated or deactivated to enhance or restrict the base system's behaviors. Features can also facilitate the analysis of families of systems by exploiting commonalities of the family members and performing an all-in-one analysis, where all systems of the family are analyzed at once on a single family model instead of one-by-one. Most prominent, the concept of features has been successfully applied to describe and analyze (software) product lines. We present the tool ProFeat that supports the feature-oriented engineering process for stochastic systems by probabilistic model checking. To describe families of stochastic systems, ProFeat extends models for the prominent probabilistic model checker Prism by feature-oriented concepts, including support for probabilistic product lines with dynamic feature switches, multi-features and feature attributes. ProFeat provides a compact symbolic representation of the analysis results for each family member obtained by Prism to support, e.g., model repair or refinement during feature-oriented development. By means of several case studies we show how ProFeat eases family-based quantitative analysis and compare one-by-one and all-in-one analysis approaches.