ProFeat: feature-oriented engineering for family-based probabilistic model checking
Tóm tắt
Từ khóa
Tài liệu tham khảo
Apel S Janda F Trujillo S Kästner C (2009) Model superimposition in software product lines. In: ICMT’09 volume 5563 of LNCS pp 4–19. Springer Berlin
Apel S von Rhein A Wendler P Groesslinger A Beyer D (2013) Strategies for product-line verification: case studies and experiments. In: Proceedings of the 2013 international conference on software engineering ICSE ’13. IEEE pp 482–491
Apel S Speidel H Wendler P von Rhein A Beyer D (2011) Detection of feature interactions using feature-aware verification. In: International conference on automated software engineering (ASE). IEEE pp 372–375
Asirelli P ter Beek MH Gnesi S Fantechi A (2011) Formal description of variability in product families. In: Proceedings of the 2011 15th international software product line conference SPLC ’11. IEEE Computer Society Washington DC USA pp 130–139
Bianco A de Alfaro L (1995) Model checking of probabilistic and non-deterministic systems. In: FSTTCS’95 volume 1026 of LNCS pp 499–513
Baier C Daum M Dubslaff C Klein J Klüppelholz S (2014) Energy-utility quantiles. Springer Berlin pp 285–299
Baier C Engel B Klüppelholz S Märcker S Tews H Völp M (2013) A probabilistic quantitative analysis of probabilistic-write/copy-select. In: Proceedings of the 5th NASA formal methods symposium (NFM) LNCS. Springer pp 307–321
Baier C, 2008, Principles of model checking
Cordy M Classen A Heymans P Legay A Schobbens P-Y (2013) Model checking adaptive software with featured transition systems. LNCS. Springer Berlin pp 1–29
Cordy M Classen A Heymans P Schobbens P-Y Legay A (2013) ProVeLines: a product line of verifiers for software product lines. In: 17th International software product line conference (SPLC). ACM pp 141–146
Chrszon P Dubslaff C Klüppelholz S Baier C (2016) Family-based modeling and analysis for probabilistic systems—featuring ProFeat. Springer Berlin pp 287–304
Clarke EM Fujita M McGeers PC McMillan KL Yang JC-Y Zhao X-J (1993) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. In: Proceedings of international workshop on logic and synthesis
Classen A Heymans P Schobbens P-Y Legay A Raskin J-F (2010) Model checking lots of systems: efficient verification of temporal properties in software product lines. In: 32nd International conference on software engineering (ICSE). ACM pp 335–344
Clements P Northrop L (2001) Software product lines: practices and patterns. Addison-Wesley Professional Reading
Cordy M Schobbens P-Y Heymans P Legay A (2013) Beyond boolean product-line model checking: dealing with feature attributes and multi-features. In: Proceedings of the 2013 international conference on software engineering ICSE ’13. IEEE Press pp 472–481
Dimovski AS Al-Sibahi AS Brabrand C Wasowski A (2015) Family-based model checking without a family-based model checker. In: Model checking software—22nd international symposium SPIN 2015 Stellenbosch South Africa August 24–26 2015 Proceedings pp 282–299
Daws C (2004) Symbolic and parametric model checking of discrete-time Markov chains. In: Theoretical aspects of computing—ICTAC 2004 volume 3407 of LNCS pp 280–294
Dubslaff C, 2015, Probabilistic model checking for feature-oriented systems, Trans Aspect-Oriented Softw Dev XII,, 8989, 180, 10.1007/978-3-662-46734-3_5
Dehnert C Junges S Jansen N Corzilius F Volk M Bruintjes H Katoen J-P Abraham E (2015) PROPhESY: a probabilistic parameter synthesis tool. In: 27th International conference on computer aided verification (CAV) volume 9206 of LNCS pp 214–231
Dehnert C Junges S Katoen J-P Volk M (2016) The probabilistic model checker Storm (extended abstract). arXiv:1610.08713
Dubslaff C Klüppelholz S Baier C (2014) Probabilistic model checking for energy analysis in software product lines. In: 13th International conference on modularity MODULARITY ’14 Lugano Switzerland April 22–26 2014 pp 169–180
Dinkelaker T Mitschke R Fetzer K Mezini M (2010) A dynamic software product line approach using aspect models at runtime. In: Proceedings of the 1st workshop on composition and variability
Damiani F Schaefer I (2011) Dynamic delta-oriented programming. In: Proceedings of the 15th International software product line conference SPLC ’11. ACM
Filieri A, 2012, A formal approach to adaptive software: continuous assurance of non-functional requirements, Form Asp Comput, 24, 163, 10.1007/s00165-011-0207-2
Gomaa H Hussein M (2003) Dynamic software reconfiguration in software product families. In: PFE pp 435–444
Hahn EM Hermanns H Wachter B Zhang L (2010) PARAM: A model checker for parametric Markov models. In: 22nd International conference on computer aided verification (CAV) volume 6174 of LNCS pp 660–664
Klein J Baier C Chrszon P Daum M Dubslaff C Klüppelholz S Märcker S Müller D (2016) Advances in symbolic probabilistic model checking with PRISM. In: Tools and algorithms for the construction and analysis of systems—22nd international conference TACAS 2016 Proceedings pp 349–366
Kang KC Cohen SG Hess JA Novak WE Peterson AS (1990) Feature-oriented domain analysis (FODA) feasibility study. Technical Report CMU/SEI-90-TR-21 Carnegie-Mellon University
Kwiatkowska M Norman G Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan G Qadeer S (eds) Proceedings of 23rd international conference on computer aided verification (CAV’11) volume 6806 of LNCS. Springer pp 585–591
Kwiatkowska MZ Norman G Parker D (2012) The PRISM benchmark suite. In: Proceedings of quantitative evaluation of systems (QEST’12) pp 203–204. IEEE https://github.com/prismmodelchecker/prism-benchmarks/.
Kowal M Schaefer I Tribastone M (2014) Family-based performance analysis of variant-rich software systems. In: Fundamental approaches to software engineering volume 8411 of LNCS pp 94–108
Legay A Perrouin G (2017) On quantitative requirements for product lines. In: Proceedings of the eleventh international workshop on variability modelling of software-intensive systems VAMOS ’17 New York NY USA. ACM pp 2–4
Lauenroth K Pohl K Toehning S (2009) Model checking of domain artifacts in product line engineering. In: 24th IEEE/ACM international conference on automated software engineering (ASE). IEEE pp 269–280
Panda S Somenzi F (1995) Who are the variables in your neighborhood. In: Proceedings of computer-aided design (ICCAD’95). IEEE pp 74–77
Rodrigues GN Alves V Nunes V Lanna A Cordy M Schobbens P-Y Sharifloo AM Legay A (2015) Modeling and verification for probabilistic properties in software product lines. In: High assurance systems engineering (HASE). IEEE pp 173–180
Rudell R (1993) Dynamic variable ordering for ordered binary decision diagrams. In: IEEE/ACM international conference on computer-aided design (ICCAD-93) pp 42–47
Schaefer I (2010) Variability modelling for model-driven development of software product lines. In: VaMoS
Segura S (2008) Automated analysis of feature models using atomicsets. In: SPLC (2) pp 201--207
Thüm T Apel S Kästner C Schaefer I Saake G (June 2014) A classification and survey of analysis strategies for software product lines. ACM Comput Surv 47(1):6:1–6:45
ter Beek MH Legay A Lluch-Lafuente A Vandin A (2015) Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: 19th International conference on software product line (SPLC). ACM pp 11–15
ter Beek MH Mazzanti F Sulova A (2012) VMC: a tool for product variability analysis. Springer Berlin pp 450–454
Thüm T Kästner C Benduhn F Meinicke J Saake G Leich T (2014) FeatureIDE: an extensible framework for feature-oriented software development. Sci Comput Program 79:70–85
von Rhein Alexander (2016) Analysis strategies for configurable systems. PhD thesis University of Passau