- AutorIn
- Philipp Chrszon Technische Universität, Professur für Algebraische und logische Grundlagen der Informatik
- Clemens DubslaffTechnische Universität, Professur für Algebraische und logische Grundlagen der Informatik
- Dr.-Ing. Sascha KlüppelholzTechnische Universität, Professur für Algebraische und logische Grundlagen der Informatik
- Prof. Dr. Christel Baier
- Titel
- ProFeat
- Untertitel
- Feature-oriented engineering for family-based probabilistic model checking
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-707928
- Quellenangabe
- Formal Aspects of Computing : Applicable Formal Methods
Erscheinungsort: London
Verlag: Springer
Erscheinungsjahr: 2018
Jahrgang: 30
Heft: 1
Seiten: 45-75
E-ISSN: 1433-299X - Erstveröffentlichung
- 2017
- Abstract (EN)
- 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.
- Andere Ausgabe
- Link zum Artikel, der zuerst in der Zeitschrift 'Formal Aspects of Computing' erschienen ist.
DOI: 10.1007/s00165-017-0432-4 - Freie Schlagwörter (DE)
- Formale Methoden, Verifikation, Quantitative Analyse, Model Checking, Feature-orientierte Systeme, Softwareproduktlinien
- Freie Schlagwörter (EN)
- formal methods, verification, quantitative analysis, model checking, feature-oriented systems, software product lines
- Klassifikation (DDC)
- 004
- Verlag
- Springer, London
- Version / Begutachtungsstatus
- angenommene Version / Postprint / Autorenversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-707928
- Veröffentlichungsdatum Qucosa
- 11.05.2020
- Dokumenttyp
- Artikel
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis