Skip to main content
Erschienen in: International Journal on Software Tools for Technology Transfer 5/2017

26.05.2016 | Regular Paper

Efficient family-based model checking via variability abstractions

verfasst von: Aleksandar S. Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, Andrzej Wąsowski

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 5/2017

Einloggen

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Many software systems are variational: they can be configured to meet diverse sets of requirements. They can produce a (potentially huge) number of related systems, known as products or variants, by systematically reusing common parts. For variational models (variational systems or families of related systems), specialized family-based model checking algorithms allow efficient verification of multiple variants, simultaneously, in a single run. These algorithms, implemented in a tool \(\overline{\text {SNIP}}\), scale much better than “the brute force” approach, where all individual systems are verified using a single-system model checker, one-by-one. Nevertheless, their computational cost still greatly depends on the number of features and variants. For variational models with a large number of features and variants, the family-based model checking may be too costly or even infeasible. In this work, we address two key problems of family-based model checking. First, we improve scalability by introducing abstractions that simplify variability. Second, we reduce the burden of maintaining specialized family-based model checkers, by showing how the presented variability abstractions can be used to model check variational models using the standard version of (single-system) SPIN. The variability abstractions are first defined as Galois connections on semantic domains. We then show how to use them for defining abstract family-based model checking, where a variability model is replaced with an abstract version of it, which preserves the satisfaction of LTL properties. Moreover, given an abstraction, we define a syntactic source-to-source transformation on high-level modeling languages that describe variational models, such that the model checking of the transformed high-level variational model coincides with the abstract model checking of the concrete high-level variational model. This allows the use of SPIN with all its accumulated optimizations for efficient verification of variational models without any knowledge about variability. We have implemented the transformations in a prototype tool, and we illustrate the practicality of this method in several case studies.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
The project on development of \(\overline{\text {SNIP}}\) model checker (https://​projects.​info.​unamur.​be/​fts/​) is independent of SPIN. \(\overline{\text {SNIP}}\) has been implemented from scratch. We put a line over \(\overline{\text {SNIP}}\) to make the distinction from SPIN clearer.
 
2
Alternatively, we could work with the set-theoretic definition of propositional formulae and consider an isomorphic complete lattice of sets of configurations \(( \left[ \! \left[ \,\, FeatExp(\mathbb {F}) \,\,\right] \! \right] ,\subseteq ,\cup ,\cap ,2^{\mathbb {F}},\emptyset )\). Here, \( \left[ \! \left[ \,\, FeatExp(\mathbb {F}) \,\,\right] \! \right] = 2^{2^{\mathbb {F}}}\), and an element of \( \left[ \! \left[ \,\, FeatExp(\mathbb {F}) \,\,\right] \! \right] \) is a subset of \(Eval(\mathbb {F})=2^{\mathbb {F}}\), which corresponds to a propositional formula over \(\mathbb {F} \) which is satisfied by those evaluations.
 
3
The \(f\) Promela Reconfigurator tool is available from: https://​models-team.​github.​io/​p3-tool/​.
 
Literatur
1.
Zurück zum Zitat Apel, S., Batory, D.S., Kästner, C., Saake, G.: Feature-oriented software product lines—concepts and implementation. Springer (2013) Apel, S., Batory, D.S., Kästner, C., Saake, G.: Feature-oriented software product lines—concepts and implementation. Springer (2013)
2.
Zurück zum Zitat Apel, S., Speidel, H., Wendler, P., von Rhein, A., Beyer, D.: Detection of feature interactions using feature-aware verification. In: 26th IEEE/ACM international conference on automated software engineering (ASE 2011), pp. 372–375 (2011) Apel, S., Speidel, H., Wendler, P., von Rhein, A., Beyer, D.: Detection of feature interactions using feature-aware verification. In: 26th IEEE/ACM international conference on automated software engineering (ASE 2011), pp. 372–375 (2011)
3.
Zurück zum Zitat Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008) Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)
4.
Zurück zum Zitat Belder, T., ter Beek, M.H., de Vink, E.P.: Coherent branching feature bisimulation. In: Proceedings 6th workshop on formal methods and analysis in SPL engineering, FMSPLE 2015, EPTCS, vol. 182, pp.14–30 (2015) Belder, T., ter Beek, M.H., de Vink, E.P.: Coherent branching feature bisimulation. In: Proceedings 6th workshop on formal methods and analysis in SPL engineering, FMSPLE 2015, EPTCS, vol. 182, pp.14–30 (2015)
5.
Zurück zum Zitat Bodden, E., Tolêdo, T., Ribeiro, M., Brabrand, C., Borba, P., Mezini, M.: Spl\({}^{\text{lift}}\): statically analyzing software product lines in minutes instead of years. In: ACM SIGPLAN Conference on PLDI ’13, pp. 355–364 (2013) Bodden, E., Tolêdo, T., Ribeiro, M., Brabrand, C., Borba, P., Mezini, M.: Spl\({}^{\text{lift}}\): statically analyzing software product lines in minutes instead of years. In: ACM SIGPLAN Conference on PLDI ’13, pp. 355–364 (2013)
6.
Zurück zum Zitat Brabrand, C., Ribeiro, M., Tolêdo, T., Winther, J., Borba, P.: Intraprocedural dataflow analysis for software product lines. Trans. Aspect Oriented Soft. Dev. 10, 73–108 (2013) Brabrand, C., Ribeiro, M., Tolêdo, T., Winther, J., Borba, P.: Intraprocedural dataflow analysis for software product lines. Trans. Aspect Oriented Soft. Dev. 10, 73–108 (2013)
7.
Zurück zum Zitat Chen, S., Erwig, M., Walkingshaw, E.: An error-tolerant type system for variational lambda calculus. In: ACM SIGPLAN international conference on functional programming, ICFP’12, pp. 29–40 (2012) Chen, S., Erwig, M., Walkingshaw, E.: An error-tolerant type system for variational lambda calculus. In: ACM SIGPLAN international conference on functional programming, ICFP’12, pp. 29–40 (2012)
8.
Zurück zum Zitat Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. STTT 2(4), 410–425 (2000)CrossRefMATH Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. STTT 2(4), 410–425 (2000)CrossRefMATH
9.
Zurück zum Zitat Clarke, Edmund M., Grumberg, Orna, Long, David E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)CrossRef Clarke, Edmund M., Grumberg, Orna, Long, David E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)CrossRef
10.
Zurück zum Zitat Classen, A., Boucher, Q., Heymans, P.: A text-based approach to feature modelling: syntax and semantics of TVL. Sci. Comput. Program. 76(12), 1130–1143 (2011)CrossRef Classen, A., Boucher, Q., Heymans, P.: A text-based approach to feature modelling: syntax and semantics of TVL. Sci. Comput. Program. 76(12), 1130–1143 (2011)CrossRef
11.
Zurück zum Zitat Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y.: model checking software product lines with SNIP. STTT 14(5), 589–612 (2012)CrossRef Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y.: model checking software product lines with SNIP. STTT 14(5), 589–612 (2012)CrossRef
12.
Zurück zum Zitat 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. Software Eng. 39(8), 1069–1089 (2013)CrossRef 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. Software Eng. 39(8), 1069–1089 (2013)CrossRef
13.
Zurück zum Zitat Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: Symbolic model checking of software product lines. In: Proceedings of the 33rd international conference on software engineering, ICSE 2011, pp. 321–330 (2011) Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: Symbolic model checking of software product lines. In: Proceedings of the 33rd international conference on software engineering, ICSE 2011, pp. 321–330 (2011)
14.
Zurück zum Zitat Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A., Raskin, J.-F.: 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, ICSE 2010, pp. 335–344 (2010) Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A., Raskin, J.-F.: 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, ICSE 2010, pp. 335–344 (2010)
15.
Zurück zum Zitat Clements, P., Northrop, L.: Software product lines: practices and patterns. Addison-Wesley (2001) Clements, P., Northrop, L.: Software product lines: practices and patterns. Addison-Wesley (2001)
16.
Zurück zum Zitat Cordy, M., Classen, A., Perrouin, G., Schobbens, P.-Y., Heymans, P., Legay, A.: Simulation-based abstractions for software product-line model checking. In: Proceedings of the 34th international conference on software engineering, ICSE 2012, pp. 672–682 (2012) Cordy, M., Classen, A., Perrouin, G., Schobbens, P.-Y., Heymans, P., Legay, A.: Simulation-based abstractions for software product-line model checking. In: Proceedings of the 34th international conference on software engineering, ICSE 2012, pp. 672–682 (2012)
17.
Zurück zum Zitat Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y., Dawagne, B., Leucker, M.: Counterexample guided abstraction refinement of product-line behavioural models. In: Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, (FSE-22), pp. 190–201 (2014) Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y., Dawagne, B., Leucker, M.: Counterexample guided abstraction refinement of product-line behavioural models. In: Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, (FSE-22), pp. 190–201 (2014)
18.
Zurück zum Zitat Cousot, P,: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational system design. NATO ASI Series F. IOS Press, Amsterdam (1999) Cousot, P,: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational system design. NATO ASI Series F. IOS Press, Amsterdam (1999)
19.
Zurück zum Zitat Czarnecki, K., Antkiewicz, M.: Mapping features to models: a template approach based on superimposed variants. In: Generative programming and component engineering, 4th Int. Conf., GPCE 2005, LNCS, vol. 3676, pp. 422–437 (2005) Czarnecki, K., Antkiewicz, M.: Mapping features to models: a template approach based on superimposed variants. In: Generative programming and component engineering, 4th Int. Conf., GPCE 2005, LNCS, vol. 3676, pp. 422–437 (2005)
20.
Zurück zum Zitat Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19(2), 253–291 (1997)CrossRef Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19(2), 253–291 (1997)CrossRef
21.
22.
Zurück zum Zitat Dimovski, A.S.: Symbolic game semantics for model checking program families. In: Model Checking Software—23nd International Symposium, SPIN 2016, Proceedings, LNCS, vol. 9641, pp. 19–37. Springer (2016) Dimovski, A.S.: Symbolic game semantics for model checking program families. In: Model Checking Software—23nd International Symposium, SPIN 2016, Proceedings, LNCS, vol. 9641, pp. 19–37. Springer (2016)
23.
Zurück zum Zitat Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wasowski, A.: Family-based model checking without a family-based model checker. In: Model checking software—22nd International Symposium, SPIN 2015, Proceedings, LNCS, vol. 9232, pp. 282–299. Springer (2015) Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wasowski, A.: Family-based model checking without a family-based model checker. In: Model checking software—22nd International Symposium, SPIN 2015, Proceedings, LNCS, vol. 9232, pp. 282–299. Springer (2015)
24.
Zurück zum Zitat Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions: trading precision for speed in family-based analyses. In: 29th European conference on object-oriented programming, ECOOP 2015, LIPIcs, vol. 37, pp. 247–270. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015) Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions: trading precision for speed in family-based analyses. In: 29th European conference on object-oriented programming, ECOOP 2015, LIPIcs, vol. 37, pp. 247–270. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)
25.
Zurück zum Zitat Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions: trading precision for speed in family-based analyses (extended version). CoRR, abs/1503.04608 (2015) Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions: trading precision for speed in family-based analyses (extended version). CoRR, abs/1503.04608 (2015)
26.
Zurück zum Zitat Fantechi, A., Gnesi, S.: A behavioural model for product families. In: Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007, pp. 521–524. ACM (2007) Fantechi, A., Gnesi, S.: A behavioural model for product families. In: Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007, pp. 521–524. ACM (2007)
27.
Zurück zum Zitat Gallardo, M., Martínez, J., Merino, P., Pimentel, E.: \(\alpha \)spin: a tool for abstract model checking. STTT 5(2–3), 165–184 (2004)CrossRef Gallardo, M., Martínez, J., Merino, P., Pimentel, E.: \(\alpha \)spin: a tool for abstract model checking. STTT 5(2–3), 165–184 (2004)CrossRef
28.
Zurück zum Zitat Gallardo, M., Merino, P., Pimentel, E.: Refinement of LTL formulas for abstract model checking. In: Static analysis, 9th international symposium, SAS 2002, Proceedings, LNCS, vol. 2477, pp. 395–410. Springer (2002) Gallardo, M., Merino, P., Pimentel, E.: Refinement of LTL formulas for abstract model checking. In: Static analysis, 9th international symposium, SAS 2002, Proceedings, LNCS, vol. 2477, pp. 395–410. Springer (2002)
29.
Zurück zum Zitat Gruler, A., Leucker, M., Scheidemann, K.D.: Modeling and model checking software product lines. In: Formal methods for open object-based distributed systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Proceedings, LNCS, vol. 5051, pp. 113–131. Springer (2008) Gruler, A., Leucker, M., Scheidemann, K.D.: Modeling and model checking software product lines. In: Formal methods for open object-based distributed systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Proceedings, LNCS, vol. 5051, pp. 113–131. Springer (2008)
30.
Zurück zum Zitat Holzmann, G.J.: The SPIN Model Checker—primer and reference manual. Addison-Wesley (2004) Holzmann, G.J.: The SPIN Model Checker—primer and reference manual. Addison-Wesley (2004)
31.
Zurück zum Zitat Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Spencer Peterson, A.: Feature-oriented domain analysis (FODA) feasibility study. Technical report, Carnegie-Mellon University Software Engineering Institute (1990) Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Spencer Peterson, A.: Feature-oriented domain analysis (FODA) feasibility study. Technical report, Carnegie-Mellon University Software Engineering Institute (1990)
32.
Zurück zum Zitat Kästner, C., Apel, S., Thüm, T., Saake, G.: Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol. 21(3), 14 (2012)CrossRef Kästner, C., Apel, S., Thüm, T., Saake, G.: Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol. 21(3), 14 (2012)CrossRef
33.
Zurück zum Zitat Kästner, C., Giarrusso, P.G., Rendel, T., Erdweg, S., Ostermann, K., Berger, T.: 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 (2011) Kästner, C., Giarrusso, P.G., Rendel, T., Erdweg, S., Ostermann, K., Berger, T.: 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 (2011)
34.
Zurück zum Zitat Kramer, J., Magee, J., Sloman, M., Lister, A.: Conic: An integrated approach to distributed computer control systems. IEE Proc. 130(1), 1–10 (1983)CrossRef Kramer, J., Magee, J., Sloman, M., Lister, A.: Conic: An integrated approach to distributed computer control systems. IEE Proc. 130(1), 1–10 (1983)CrossRef
35.
Zurück zum Zitat Lauenroth, K., Pohl, K., Toehning, S.: Model checking of domain artifacts in product line engineering. In: ASE 2009, 24th IEEE/ACM International Conference on Automated Software Engineering, 2009, pp. 269–280. IEEE Computer Society (2009) Lauenroth, K., Pohl, K., Toehning, S.: Model checking of domain artifacts in product line engineering. In: ASE 2009, 24th IEEE/ACM International Conference on Automated Software Engineering, 2009, pp. 269–280. IEEE Computer Society (2009)
36.
Zurück zum Zitat Lochau, M., Mennicke, S., Baller, H., Ribbeck, L.: Incremental model checking of delta-oriented software product lines. J. Log. Algebraic Methods Program. 85(1), 245–267 (2016)MathSciNetCrossRefMATH Lochau, M., Mennicke, S., Baller, H., Ribbeck, L.: Incremental model checking of delta-oriented software product lines. J. Log. Algebraic Methods Program. 85(1), 245–267 (2016)MathSciNetCrossRefMATH
37.
Zurück zum Zitat Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des. 6(1), 11–44 (1995)CrossRefMATH Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des. 6(1), 11–44 (1995)CrossRefMATH
38.
Zurück zum Zitat McMillan, K.L.: Applications of craig interpolants in model checking. In: Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Proceedings, LNCS, vol. 3440, pp. 1–12. Springer (2005) McMillan, K.L.: Applications of craig interpolants in model checking. In: Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Proceedings, LNCS, vol. 3440, pp. 1–12. Springer (2005)
39.
Zurück zum Zitat Midtgaard, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program. 105, 145–170 (2015)CrossRef Midtgaard, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program. 105, 145–170 (2015)CrossRef
40.
Zurück zum Zitat Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)CrossRefMATH Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)CrossRefMATH
41.
Zurück zum Zitat Post, H., Sinz, C.: Configuration lifting: verification meets software configuration. In: 23rd IEEE/ACM international conference on automated software engineering (ASE 2008), pp. 347–350 (2008) Post, H., Sinz, C.: Configuration lifting: verification meets software configuration. In: 23rd IEEE/ACM international conference on automated software engineering (ASE 2008), pp. 347–350 (2008)
42.
Zurück zum Zitat ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Using FMC for family-based analysis of software product lines. In: Proceedings of the 19th international conference on software product line, SPLC 2015, pp. 432–439. ACM (2015) ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Using FMC for family-based analysis of software product lines. In: Proceedings of the 19th international conference on software product line, SPLC 2015, pp. 432–439. ACM (2015)
43.
Zurück zum Zitat ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebraic Methods Program. 85(2), 287–315 (2016)MathSciNetCrossRefMATH ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebraic Methods Program. 85(2), 287–315 (2016)MathSciNetCrossRefMATH
44.
Zurück zum Zitat Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6 (2014)CrossRef Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6 (2014)CrossRef
45.
Zurück zum Zitat Thüm, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: Generative programming and component engineering, GPCE’12, pp. 11–20. ACM (2012) Thüm, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: Generative programming and component engineering, GPCE’12, pp. 11–20. ACM (2012)
46.
Zurück zum Zitat Thüm, T., Winkelmann, T., Schröter, R., Hentschel, M., Krüger, S.: Variability hiding in contracts for dependent software product lines. In: Proceedings of the tenth international workshop on variability modelling of software-intensive systems, 2016, pp. 97–104. ACM (2016) Thüm, T., Winkelmann, T., Schröter, R., Hentschel, M., Krüger, S.: Variability hiding in contracts for dependent software product lines. In: Proceedings of the tenth international workshop on variability modelling of software-intensive systems, 2016, pp. 97–104. ACM (2016)
Metadaten
Titel
Efficient family-based model checking via variability abstractions
verfasst von
Aleksandar S. Dimovski
Ahmad Salim Al-Sibahi
Claus Brabrand
Andrzej Wąsowski
Publikationsdatum
26.05.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 5/2017
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-016-0425-2

Weitere Artikel der Ausgabe 5/2017

International Journal on Software Tools for Technology Transfer 5/2017 Zur Ausgabe