×

zbMATH — the first resource for mathematics

Finding suitable variability abstractions for lifted analysis. (English) Zbl 1425.68067
Summary: Many software systems are today variational: they are built as program families or Software Product Lines. They can produce a potentially huge number of related programs, known as products or variants, by selecting suitable configuration options (features) at compile time. Many such program families are safety critical, yet the appropriate tools only rarely are able to analyze them efficiently. Researchers have addressed this problem by designing specialized <span class=”textit”>v</span>ariability-aware static (dataflow) analyses, which allow analyzing all variants of the family, simultaneously, in a single run without generating any of the variants explicitly. They are also known as <span class=”textit”>l</span>ifted or <span class=”textit”>f</span>amily-based analyses. They take as input the common code base, which encodes all variants of a program family, and produce precise analysis results corresponding to all variants. These analyses scale much better than “brute force” approach, where all individual variants are analyzed in isolation, one-by-one, using off-the-shelf single-program analyzers. Nevertheless, the computational cost of lifted analyses still greatly depends on the number of features and variants (which is often huge). For families with a large number of features and variants, the lifted analyses may be too costly or even infeasible. In order to speed up lifted analyses and make them computationally cheaper, variability abstractions which simplify variability away from program families and lifted analyses have been introduced. However, the space of possible variability abstractions is still intractably large to search naively, with most abstractions being either too imprecise or too costly.
We introduce here a method to efficiently find suitable variability abstractions from a large space of possible abstractions for a lifted static analysis. The main idea is to use a <span class=”textit”>p</span>re-analysis to estimate the impact of variability-specific parts of the program family on the analysis’s precision. The pre-analysis is fully variability-aware while it aggressively abstracts the other semantics aspects. Then we use the pre-analysis results to find out when and where the subsequent abstract lifted analysis should turn off or on its variability-awareness. The abstraction constructed in this way is effective in discarding variability-specific program details that are irrelevant for showing the analysis’s ultimate goal. We formalize this approach and we illustrate its effectiveness on several Java case studies. The evaluation shows that our approach which consists of running a pre-analysis followed by a subsequent abstract lifted analysis achieves competitive the precision-speed tradeoff compared to the standard lifted analysis.

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Software:
Apron; Soot; Sparrow; SPIN
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Apel, S.; Kästner, C., An overview of feature-oriented software development, J Object Technol, 8, 49-84, (2009)
[2] Batory D (2005) Feature models, grammars, and propositional formulas. In: 9th International software product lines conference, SPLC ’05, volume 3714 of LNCS, Springer-Verlag, pp 7-20
[3] Brabrand, C.; Ribeiro, M.; Tolêdo, T.; Winther, J.; Borba, P., Intraprocedural dataflow analysis for software product lines, Trans Asp Oriented Softw Dev, 10, 73-108, (2013)
[4] Bryant, RE, Graph-based algorithms for boolean function manipulation, IEEE Trans Comput, 35, 677-691, (1986) · Zbl 0593.94022
[5] Bodden E, Tolêdo T, Ribeiro M, Brabrand C, Borba P, Mezini M (2013) \(\text{Spl}^{{{\rm lift}}}\): statically analyzing software product lines in minutes instead of years. In: ACM SIGPLAN conference on PLDI ’13, pp 355-364
[6] Cousot, P.; Cousot, R.; Sethi, R. (ed.), Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, 238-252, (1977), California
[7] Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: POPL’79, pp 269-282 · Zbl 1323.68356
[8] Cousot, P.; Cousot, R., Abstract interpretation and application to logic programs, J Log Program, 13, 103-179, (1992) · Zbl 0776.68024
[9] Chen J, Cousot P (2015) A binary decision tree abstract domain functor. In: Static analysis—22nd international symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings, volume 9291 of LNCS, Springer, pp 36-53
[10] Classen, A.; Cordy, M.; Heymans, P.; Legay, A.; Schobbens, P-Y, Model checking software product lines with SNIP, STTT, 14, 589-612, (2012)
[11] Cousot P, Cousot R, Mauborgne L (2010) A scalable segmented decision tree abstract domain. In: Time for verification, essays in memory of Amir Pnueli, volume 6200 of LNCS, Springer, pp 72-95 · Zbl 1288.68040
[12] Classen, A.; Cordy, M.; Schobbens, P-Y; Heymans, P.; Legay, A.; Raskin, J-F, Featured transition systems: Foundations for verifying variability-intensive systems and their application to LTL model checking, IEEE Trans Softw Eng, 39, 1069-1089, (2013)
[13] Chrszon, P.; Dubslaff, C.; Klüppelholz, S.; Baier, C., Profeat: feature-oriented engineering for family-based probabilistic model checking, Formal Asp Comput, 30, 45-75, (2018)
[14] Chen S, Erwig M, Walkingshaw E (2012) An error-tolerant type system for variational lambda calculus. In: ACM SIGPLAN international conference on functional programming, ICFP’12, pp 29-40 · Zbl 1291.68111
[15] Classen A, Heymans P, Schobbens P-Y, Legay A (2011) Symbolic model checking of software product lines. In: Proceedings of the 33rd international conference on software engineering, ICSE 2011, pp 321-330
[16] Clements, P., Northrop, L.: Software product lines: practices and patterns. Addison-Wesley, Boston (2001)
[17] Cousot, P.; Broy, M. (ed.); Steinbrüggen, R. (ed.), The calculational design of a generic abstract interpreter, 1-88, (1999), Amsterdam
[18] Chechik M, Stavropoulou I, Disenfeld C, Rubin J (2018) FPH: efficient non-commutativity analysis of feature-based systems. In: Fundamental approaches to software engineering, 21st international conference, FASE 2018, proceedings., volume 10802 of LNCS, Springer, pp 319-336
[19] Cordy M, Schobbens P-Y, Heymans P, Legay A (2012) Behavioural modelling and verification of real-time software product lines. In: 16th International software product line conference, SPLC ’12, Vol 1. ACM, pp 66-75
[20] 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, proceedings, volume 9232 of LNCS, Springer, pp 282-299
[21] Dimovski, A.; Al-Sibahi, AS; Brabrand, C.; Wasowski, A., Efficient family-based model checking via variability abstractions, STTT, 19, 585-603, (2017)
[22] Dimovski AS, Brabrand C, Wasowski A (2015) Variability abstractions: trading precision for speed in family-based analyses. In: 29th European conference on object-oriented programming, ECOOP 2015, volume 37 of LIPIcs, Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik, pp 247-270
[23] Dimovski AS, Brabrand C, Wasowski A (2016) Finding suitable variability abstractions for family-based analysis. In: FM 2016: formal methods—21st international symposium, proceedings, volume 9995 of LNCS, pp 217-234
[24] Dimovski, AS; Brabrand, C.; Wasowski, A., Variability abstractions for lifted analysis, Sci Comput Program, 159, 1-27, (2018)
[25] Dimovski, A., Program verification using symbolic game semantics, Theor Comput Sci, 560, 364-379, (2014) · Zbl 1303.68083
[26] Dimovski AS (2016) Symbolic game semantics for model checking program families. In: Model checking software—23nd international symposium, SPIN 2016, proceedings, volume 9641 of LNCS, Springer, pp 19-37
[27] Dimovski AS (2018) Abstract family-based model checking using modal featured transition systems: preservation of . In: Fundamental approaches to software engineering, 21st international conference, FASE 2018, proceedings., volume 10802 of LNCS, Springer, pp 301-318
[28] Dimovski, AS, Verifying annotated program families using symbolic game semantics, Theor Comput Sci, 706, 35-53, (2018) · Zbl 1380.68121
[29] Dimovski AS, Wasowski A (2017) From transition systems to variability models and from lifted model checking back to UPPAAL. In: Models, algorithms, logics and tools—essays dedicated to kim guldstrand Larsen on the occasion of his 60th birthday, volume 10460 of LNCS, Springer, pp 249-268
[30] Dimovski AS, Wasowski A (2017) Variability-specific abstraction refinement for family-based model checking. In: Fundamental approaches to software engineering—20th international conference, FASE 2017, proceedings, volume 10202 of LNCS, pp 406-423
[31] Erwig M, Walkingshaw E (2011) The choice calculus: a representation for software variation. ACM Trans Softw Eng Methodol 21(1):6:1-6:27
[32] Gazzillo P, Grimm R (2012) Superc: parsing all of C by taming the preprocessor. In: Vitek J, Lin H, Tip F (eds) ACM SIGPLAN conference on programming language design and implementation, PLDI ’12, Beijing, China—June 11-16, 2012, ACM, pp 323-334
[33] Iosif-Lazar AF, Al-Sibahi AS, Dimovski AS, Savolainen JE, Sierszecki K, Wasowski A (2015) Experiences from designing and validating a software modernization transformation (E). In: 30th IEEE/ACM International conference on automated software engineering, ASE 2015, pp 597-607
[34] Iosif-Lazar, AF; Melo, J.; Dimovski, AS; Brabrand, C.; Wasowski, A., Effective analysis of c programs by rewriting variability, Program J, 1, 1, (2017)
[35] Jeannet B, Miné A (2009) Apron: a library of numerical abstract domains for static analysis. In: Computer aided verification, 21st international conference, CAV 2009. Proceedings, volume 5643 of LNCS, Springer, pp 661-667
[36] Christian K, Apel S (2008) Type-checking software product lines—a formal approach. In: 23rd IEEE/ACM international conference on automated software engineering (ASE) 2008), pp 258-267
[37] Kästner C, Apel S, Kuhlemann M (2008) Granularity in software product lines. In: Proceedings of the 30th international conference on software engineering (ICSE’08), Leipzig, Germany, ACM, pp 311-320
[38] Kastner C (2010) Virtual separation of concerns: toward preprocessors 2.0. Ph.D. thesis, University of Magdeburg, Germany
[39] Kästner C, Giarrusso PG, Rendel T, Erdweg S, Ostermann K, Berger T (2011) Variability-aware parsing in the presence of lexical macros and conditional compilation. In: Proceedings of the 26th annual ACM SIGPLAN conference on object-oriented programming, systems, languages, and applications, OOPSLA 2011, part of SPLASH 2011, pp 805-824
[40] Larsen KG, Nyman U, Wasowski A (2007) Modal I/O automata for interface and product line theories. In: Programming languages and systems, 16th European symposium on programming, ESOP 2007, proceedings, volume 4421 of LNCS, Springer, pp 64-79 · Zbl 1187.68296
[41] Liang P, Tripp O, Naik M (2011) Learning minimal abstractions. In: Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2011, pp 31-42 · Zbl 1284.68519
[42] Midtgaard, J.; Dimovski, AS; Brabrand, C.; Wasowski, A., Systematic derivation of correct variability-aware program analyses, Sci Comput Program, 105, 145-170, (2015)
[43] Meinicke J, Wong C-P, Kästner C, Thüm T, Saake G (2016) On essential configuration complexity: measuring interactions in highly-configurable systems. In: Proceedings of the 31st IEEE/ACM international conference on automated software engineering, ASE 2016, Singapore, September 3-7, 2016, ACM, pp 483-494
[44] Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis. Springer, Secaucus (1999) · Zbl 0932.68013
[45] Naik M, Yang H, Castelnuovo G, Sagiv M (2012) Abstractions from tests. In: Proceedings of the 39th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2012, pp 373-386
[46] Oh H, Lee W, Heo K, Yang H, Yi K (2014) Selective context-sensitivity guided by impact pre-analysis. In: ACM SIGPLAN conference on programming language design and implementation, PLDI ’14, p 49
[47] Oh, H.; Lee, W.; Heo, K.; Yang, H.; Yi, K., Selective x-sensitive analysis guided by impact pre-analysis, ACM Trans Program Lang Syst, 38, 6, (2016)
[48] Dalla Preda, M.; Giacobazzi, R.; Debray, SK, Unveiling metamorphism by abstract interpretation of code properties, Theor Comput Sci, 577, 74-97, (2015) · Zbl 1309.68044
[49] Reps T, Horwitz S, Sagiv M (1995) Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of 22nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’95, pp 49-61
[50] Rival, X.; Mauborgne, L., The trace partitioning abstract domain, ACM Trans Program Lang Syst, 29, 26, (2007)
[51] Scholz W, Thüm T, Apel S, Lengauer C (2011) Automatic detection of feature interactions using the java modeling language: an experience report. In: Software product lines—15th international conference, SPLC 2011, workshop proceedings, Vol 2. ACM, p 7
[52] Thüm T, Apel S, Kästner C, Schaefer I, Saake G (2014) A classification and survey of analysis strategies for software product lines. ACM Comput Surv 47(1):6:1-6:45
[53] Beek, MH; Fantechi, A.; Gnesi, S.; Mazzanti, F., Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints, J Log Algebr Methods Program, 85, 287-315, (2016) · Zbl 1351.68170
[54] Urban C, Miné A (2014) A decision tree abstract domain for proving conditional termination. In: Static analysis—21st international symposium, SAS 2014. Proceedings, volume 8723 of LNCS, Springer, pp 302-318
[55] von Rhein A (2016) Analysis strategies for configurable systems. Ph.D. thesis, University of Passau, Germany
[56] Vallée-Rai R, Co P, Gagnon E, Hendren L, Lam P, Sundaresan V (1999) Soot—a java bytecode optimization framework. In: Proceedings of the 1999 conference of the centre for advanced studies on collaborative research (CASCON’99), IBM Press, pp 13
[57] Winskel, G.: The formal semantics of programming languages. The MIT Press, Cambridge, Foundation of computing series (1993) · Zbl 0919.68082
[58] Zhang X, Naik M, Yang H (2013) Finding optimum abstractions in parametric dataflow analysis. In: ACM SIGPLAN conference on programming language design and implementation, PLDI ’13, pp 365-376
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.