More Web Proxy on the site http://driver.im/

research-article

Model Verification of Dynamic Software Product Lines

Authors:

Ismayle S. Santos,

Lincoln S. Rocha,

Pedro A. Santos Neto,

Rossana M. C. AndradeAuthors Info & Claims

SBES '16: Proceedings of the XXX Brazilian Symposium on Software Engineering

Pages 113 - 122

https://doi.org/10.1145/2973839.2973852

Published: 19 September 2016 Publication History

Abstract

Dynamic Software Product Lines (DSPLs) extend the concept of Software Product Lines enabling adaptation at runtime according to context changes. Such dynamic behavior is typically designed using adaptation rules, context-triggered actions responsible for features activation and deactivation at runtime. The erroneous specification and the interleaving of adaptation rules (i.e., the parallel execution of adaptation rules) can lead DSPL to reach an undesired (improperly or defective) product configuration at runtime. Thus, in order to improve the reliability of DSPL behavior, design faults must be rigorously identified and eliminated in the early stages of DSPL development. In this paper, we address this issue introducing Dynamic Feature Transition Systems (DFTSs) that allow the modeling and formal verification of the DSPLs adaptive behavior. These transition systems are derived from the adaptation rules and a Context Kripke Structure, which is a context evolution model. Furthermore, we formally define five properties that can be used to identify existing design faults in DSPL design. Aiming to assess the feasibility of our approach, a feasibility study was conducted using two DSPLs, Mobile Visit Guides and Car. In both cases, design faults were automatically detected indicating that our formalism can help in the detection of design faults in the DSPLs adaptive behavior.

References

[1]

C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.

Digital Library

[2]

D. Benavides, S. Segura, and A. Ruiz-Cortés. Automated analysis of feature models 20 years later: A literature review. Information Systems, 35(6):615 --636, 2010.

Digital Library

[3]

N. Bencomo, S. Hallsteinsen, and E. Santana de Almeida. A view of the dynamic software product line landscape. Computer, 45(10):36--41, Oct 2012.

Digital Library

[4]

R. Capilla, J. Bosch, P. Trinidad, A. R. Cortés, and M. Hinchey. An overview of dynamic software product line architectures and techniques: Observations from research and industry. Journal of Systems and Software, 91:3--23, 2014.

Digital Library

[5]

E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model checking. MIT Press, Cambridge, USA, 1999.

Digital Library

[6]

A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay, and J.-F. Raskin. Model checking lots of systems: Efficient verification of temporal properties in software product lines. In Proceedings of the 32Nd ACM/IEEE International Conference on Software Engineering - Volume 1, pages 335--344, NY, USA, 2010. ACM.

Digital Library

[7]

M. Cordy, A. Classen, P. Heymans, A. Legay, and P.-Y. Schobbens. Assurances for Self-Adaptive Systems: Principles, Models, and Techniques, chapter Model Checking Adaptive Software with Featured Transition Systems, pages 1--29. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013.

[8]

M. Cordy, P.-Y. Schobbens, P. Heymans, and A. Legay. Behavioural modelling and verification of real-time software product lines. In Proceedings of the 16th International Software Product Line Conference - Volume 1, pages 66--75, NY, USA, 2012. ACM.

Digital Library

[9]

K. Czarnecki and A. Wasowski. Feature diagrams and logics: There and back again. In Proceedings of the 11th International Software Product Line Conference, SPLC '07, pages 23--34, Washington, DC, USA, 2007. IEEE Computer Society.

Digital Library

[10]

A. K. Dey. Understanding and using context. Personal Ubiquitous Computing, 5(1):4--7, 2001.

Digital Library

[11]

J. Guo, J. White, G. Wang, J. Li, and Y. Wang. A genetic algorithm for optimized feature selection with resource constraints in software product lines. J. Syst. Softw., 84(12):2208--2221, Dec. 2011.

Digital Library

[12]

S. Hallsteinsen, M. Hinchey, S. Park, and K. Schmid. Dynamic software product lines. Computer, 41(4):93--95, April 2008.

Digital Library

[13]

G. Holzmann. Spin Model Checker, the: Primer and Reference Manual. Addison-Wesley Professional, first edition, 2003.

Digital Library

[14]

K. C. Kang, S. G. Cohen, J. A. Hess, W. E. Novak, and A. S. Peterson. Feature-oriented domain analysis (FODA) feasibility study. Technical Report CMU/SEI-90-TR-21, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA, 1990.

[15]

F. G. Marinho, R. M. C. Andrade, C. Werner, W. Viana, M. E. F. Maia, L. S. Rocha, E. Teixeira, J. B. F. Filho, V. L. L. Dantas, F. Lima, and S. Aguiar. Mobiline: A nested software product line for the domain of mobile and context-aware applications. Sci. Comput. Program., 78(12):2381--2398, Dec. 2013.

Digital Library

[16]

J. Mauro, M. Nieke, C. Seidl, and I. C. Yu. Context aware reconfiguration in software product lines. In Proceedings of the Tenth International Workshop on Variability Modelling of Software-intensive Systems, VaMoS '16, pages 41--48, NY, USA, 2016. ACM.

Digital Library

[17]

R. Muschevici, D. Clarke, and J. Proenca. Feature petri nets. In Proc. Int'l Workshop Formal Methods and Analysis in Software Product Line Engineering, FMSPLE '10, page 99--106, 2010.

[18]

L. S. Rocha and R. M. C. Andrade. Towards a formal model to reason about context-aware exception handling. In Proceedings of the 5th International Workshop on Exception Handling, WEH '12, pages 27--33, Piscataway, NJ, USA, 2012. IEEE Press.

Digital Library

[19]

M. Sama, S. Elbaum, F. Raimondi, D. S. Rosenblum, and Z. Wang. Context-aware adaptive applications: Fault patterns and their automated identification. IEEE Transactions on Software Engineering, 36(5):644--661, 2010.

Digital Library

[20]

M. Varshosaz and R. Khosravi. Discrete time markov chain families: Modeling and verification of probabilistic software product lines. In Proceedings of the 17th International Software Product Line Conference Co-located Workshops, SPLC '13 Workshops, pages 34--41, NY, USA, 2013. ACM.

Digital Library

Cited By

Aguayo OSepúlveda SMazo R(2024)Variability Management in Self-Adaptive Systems through Deep Learning: A Dynamic Software Product Line ApproachElectronics10.3390/electronics1305090513:5(905)Online publication date: 27-Feb-2024
https://doi.org/10.3390/electronics13050905
Aguayo OSepúlveda S(2022)Variability Management in Dynamic Software Product Lines for Self-Adaptive Systems—A Systematic MappingApplied Sciences10.3390/app12201024012:20(10240)Online publication date: 12-Oct-2022
https://doi.org/10.3390/app122010240
Valdezate ACapilla RCrespo JBarber R(2022)RuVa: A Runtime Software Variability AlgorithmIEEE Access10.1109/ACCESS.2022.317550510(52525-52536)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3175505
Show More Cited By

Model Verification of Dynamic Software Product Lines
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Logic

Recommendations

Model checking software product lines with SNIP

We present SNIP, an efficient model checker for software product lines (SPLs). Variability in software product lines is generally expressed in terms of features, and the number of potential products is exponential in the number of features. Whereas ...
Behavioural modelling and verification of real-time software product lines
SPLC '12: Proceedings of the 16th International Software Product Line Conference - Volume 1

In Software Product Line (SPL) engineering, software products are build in families rather than individually. Many critical software are nowadays build as SPLs and most of them obey hard real-time requirements. Formal methods for verifying SPLs are thus ...
Managing evolution in software product lines: a model-checking perspective
VaMoS '12: Proceedings of the 6th International Workshop on Variability Modeling of Software-Intensive Systems

In Software Product Line (SPL) engineering, similar software products are developed in families rather than individually. Developing similar software at once leads to new challenges. In particular, the model checking problem for SPL is harder because it ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

SBES '16: Proceedings of the XXX Brazilian Symposium on Software Engineering

September 2016

167 pages

ISBN:9781450342018

DOI:10.1145/2973839

Editor:
Eduardo Santanda de Almeida

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

SBC: Brazilian Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 September 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

SBES '16

SBES '16: 30th Brazilian Symposium on Software Engineering

September 19 - 23, 2016

Maringá, Brazil

Acceptance Rates

Overall Acceptance Rate 147 of 427 submissions, 34%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
188
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Aguayo OSepúlveda SMazo R(2024)Variability Management in Self-Adaptive Systems through Deep Learning: A Dynamic Software Product Line ApproachElectronics10.3390/electronics1305090513:5(905)Online publication date: 27-Feb-2024
https://doi.org/10.3390/electronics13050905
Aguayo OSepúlveda S(2022)Variability Management in Dynamic Software Product Lines for Self-Adaptive Systems—A Systematic MappingApplied Sciences10.3390/app12201024012:20(10240)Online publication date: 12-Oct-2022
https://doi.org/10.3390/app122010240
Valdezate ACapilla RCrespo JBarber R(2022)RuVa: A Runtime Software Variability AlgorithmIEEE Access10.1109/ACCESS.2022.317550510(52525-52536)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3175505
Annighoefer BReinhart JBrunner MSchulz B(2021)The Concept of an Autonomic Avionics Platform and the Resulting Software Engineering Challenges2021 International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS)10.1109/SEAMS51251.2021.00031(179-185)Online publication date: May-2021
https://doi.org/10.1109/SEAMS51251.2021.00031
de Sousa Santos Ide Jesus Souza MLuciano Carvalho MAlves Oliveira Tde Almeida Ede Castro Andrade R(2017)Dynamically Adaptable Software Is All about Modeling Contextual Variability and Avoiding FailuresIEEE Software10.1109/MS.2017.412120534:6(72-77)Online publication date: Nov-2017
https://doi.org/10.1109/MS.2017.4121205
Andrade RCarvalho Rde Araújo IOliveira KMaia M(2017)What Changes from Ubiquitous Computing to Internet of Things in Interaction Evaluation?Distributed, Ambient and Pervasive Interactions10.1007/978-3-319-58697-7_1(3-21)Online publication date: 9-Jul-2017
https://dl.acm.org/doi/10.1007/978-3-319-58697-7_1
Carvalho MSantos IMasiero PJanuario Tde Almeida Ede Alcântara dos Santos Neto Pde Castro Andrade RLopez-Herrejon R(undefined)Toffa-Das: Design-Time Trade-Off Analysis for Dynamically Adaptable SoftwareSSRN Electronic Journal10.2139/ssrn.4098743
https://doi.org/10.2139/ssrn.4098743

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten