Skip to main content

09.08.2019 | FASE 2018

\(\hbox {CTL}^{\star }\) family-based model checking using variability abstractions and modal transition systems

verfasst von: Aleksandar S. Dimovski

Erschienen in: International Journal on Software Tools for Technology Transfer

Einloggen

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

search-config
loading …

Abstract

Variational systems can produce a (potentially huge) number of related systems, known as products or variants, by using features (configuration options) to mark the variable functionality. In many of the application domains, their rigorous verification and analysis are very important, yet the appropriate tools rarely are able to analyse variational systems. Recently, this problem was addressed by designing specialized so-called family-based model checking algorithms, which allow simultaneous verification of all variants in a single run by exploiting the commonalities between the variants. Yet, their computational cost still greatly depends on the number of variants (the size of configuration space), which is often huge. Moreover, their implementation and maintenance represent a costly research and development task. One of the most promising approaches to fighting the configuration space explosion problem is variability abstractions, which simplify variability away from variational systems. In this work, we show how to achieve efficient family-based model checking of \(\hbox {CTL}^{\star }\) temporal properties using variability abstractions and off-the-shelf (single-system) tools. We use variability abstractions for deriving abstract family-based model checking, where the variability model of a variational system is replaced with an abstract (smaller) version of it, called modal transition system, which preserves the satisfaction of both universal and existential temporal properties, as expressible in \(\hbox {CTL}^{\star }\). Modal transition systems contain two kinds of transitions, termed may- and must-transitions, which are defined by the conservative (over-approximating) abstractions and their dual (under-approximating) abstractions, respectively. The variability abstractions can be combined with different partitionings of the configuration space to infer suitable divide-and-conquer verification plans for the given variational system. We illustrate the practicality of this approach for several variational systems using the standard version of (single-system) NuSMV model checker.

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
An extended version of NuSMV  [11] implements the family-based algorithm for variability models obtained by composing the basic model and all available features.
 
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, Berlin (2013)CrossRef Apel, S., Batory, D.S., Kästner, C., Saake, G.: Feature-Oriented Software Product Lines—Concepts and Implementation. Springer, Berlin (2013)CrossRef
2.
Zurück zum Zitat Apel, S., Rhein, A., von Wendler, P., Größlinger, A., Beyer, D.: Strategies for product-line verification: case studies and experiments. In: 35th International Conference on Software Engineering, ICSE ’13, pp. 482–491. IEEE Computer Society (2013) Apel, S., Rhein, A., von Wendler, P., Größlinger, A., Beyer, D.: Strategies for product-line verification: case studies and experiments. In: 35th International Conference on Software Engineering, ICSE ’13, pp. 482–491. IEEE Computer Society (2013)
3.
Zurück zum Zitat Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
4.
Zurück zum Zitat Ben-David, S., Sterin, B., Atlee, J.M., Beidu, S.: Symbolic model checking of product-line requirements using sat-based methods. In: 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Volume 1, pp. 189–199. IEEE Computer Society (2015) Ben-David, S., Sterin, B., Atlee, J.M., Beidu, S.: Symbolic model checking of product-line requirements using sat-based methods. In: 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Volume 1, pp. 189–199. IEEE Computer Society (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 Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An opensource tool for symbolic model checking. In: Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings, volume 2404 of LNCS, pp. 359–364. Springer (2002)CrossRef Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An opensource tool for symbolic model checking. In: Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings, volume 2404 of LNCS, pp. 359–364. Springer (2002)CrossRef
7.
Zurück zum Zitat Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logics of Programs, Workshop, 1981, volume 131 of Lecture Notes in Computer Science, pp. 52–71. Springer (1981) Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logics of Programs, Workshop, 1981, volume 131 of Lecture Notes in Computer Science, pp. 52–71. Springer (1981)
8.
Zurück zum Zitat Classen, A.: CTL model checking for software product lines in NuSMV. Technical Report, P-CS-TR SPLMC-00000002, University Of Namur, pp. 1–17 (2011) Classen, A.: CTL model checking for software product lines in NuSMV. Technical Report, P-CS-TR SPLMC-00000002, University Of Namur, pp. 1–17 (2011)
9.
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
10.
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. Softw. 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. Softw. Eng. 39(8), 1069–1089 (2013)CrossRef
11.
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. ACM (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. ACM (2011)
12.
Zurück zum Zitat Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley, Boston (2001) Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley, Boston (2001)
13.
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: Glinz, M., Murphy, G.C., Pezzè, M. (eds.) 34th International Conference on Software Engineering, ICSE 2012, pp. 672–682. IEEE (2012) Cordy, M., Classen, A., Perrouin, G., Schobbens, P.-Y., Heymans, P., Legay, A.: Simulation-based abstractions for software product-line model checking. In: Glinz, M., Murphy, G.C., Pezzè, M. (eds.) 34th International Conference on Software Engineering, ICSE 2012, pp. 672–682. IEEE (2012)
14.
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: Cheung, S.-C. Orso, A., Storey, M.-A.D. (eds.) Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), pp. 190–201. ACM (2014) Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y., Dawagne, B., Leucker, M.: Counterexample guided abstraction refinement of product-line behavioural models. In: Cheung, S.-C. Orso, A., Storey, M.-A.D. (eds.) Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), pp. 190–201. ACM (2014)
15.
Zurück zum Zitat Cousot, P.: Partial completeness of abstract fixpoint checking. In: Abstraction, Reformulation, and Approximation, 4th International Symposium, SARA 2000, Proceedings, volume 1864 of LNCS, pp. 1–25. Springer (2000) Cousot, P.: Partial completeness of abstract fixpoint checking. In: Abstraction, Reformulation, and Approximation, 4th International Symposium, SARA 2000, Proceedings, volume 1864 of LNCS, pp. 1–25. Springer (2000)
16.
Zurück zum Zitat Dimovski, A.S.: Abstract family-based model checking using modal featured transition systems: Preservation of ctl\(^{\star }\). In: Fundamental Approaches to Software Engineering—21st International Conference, FASE 2018, Proceedings, volume 10802 of LNCS, pp. 301–318. Springer (2018)CrossRef Dimovski, A.S.: Abstract family-based model checking using modal featured transition systems: Preservation of ctl\(^{\star }\). In: Fundamental Approaches to Software Engineering—21st International Conference, FASE 2018, Proceedings, volume 10802 of LNCS, pp. 301–318. Springer (2018)CrossRef
17.
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, volume 9232 of LNCS, pp. 282–299. Springer (2015)CrossRef 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, volume 9232 of LNCS, pp. 282–299. Springer (2015)CrossRef
18.
Zurück zum Zitat Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wasowski, A.: Efficient family-based model checking via variability abstractions. STTT 19(5), 585–603 (2017)CrossRef Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wasowski, A.: Efficient family-based model checking via variability abstractions. STTT 19(5), 585–603 (2017)CrossRef
19.
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, volume 37 of LIPIcs, 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, volume 37 of LIPIcs, pp. 247–270. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik (2015)
20.
Zurück zum Zitat Dimovski, A.S., Brabrand, C., Wasowski, A.: Finding suitable variability abstractions for family-based analysis. In: FM 2016: Formal Methods—21st International Symposium, Proceedings, volume 9995 of LNCS, pp. 217–234 (2016)CrossRef Dimovski, A.S., Brabrand, C., Wasowski, A.: Finding suitable variability abstractions for family-based analysis. In: FM 2016: Formal Methods—21st International Symposium, Proceedings, volume 9995 of LNCS, pp. 217–234 (2016)CrossRef
21.
Zurück zum Zitat Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions for lifted analyses. Sci. Comput. Program. 159, 1–27 (2018)CrossRef Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions for lifted analyses. Sci. Comput. Program. 159, 1–27 (2018)CrossRef
22.
Zurück zum Zitat Dimovski, A.S., Brabrand, C., Wasowski, A.: Finding suitable variability abstractions for lifted analysis. Formal Asp. Comput. 31(2), 231–259 (2019)MathSciNetCrossRef Dimovski, A.S., Brabrand, C., Wasowski, A.: Finding suitable variability abstractions for lifted analysis. Formal Asp. Comput. 31(2), 231–259 (2019)MathSciNetCrossRef
23.
Zurück zum Zitat Dimovski, A.S., Legay, A., Wasowski, A.: Variability abstraction and refinement for game-based lifted model checking of full CTL. In: Fundamental Approaches to Software Engineering—22nd International Conference, FASE 2019, Proceedings, volume 11424 of LNCS, pp. 192–209. Springer (2019) Dimovski, A.S., Legay, A., Wasowski, A.: Variability abstraction and refinement for game-based lifted model checking of full CTL. In: Fundamental Approaches to Software Engineering—22nd International Conference, FASE 2019, Proceedings, volume 11424 of LNCS, pp. 192–209. Springer (2019)
24.
Zurück zum Zitat Dimovski, A.S., Wasowski, A.: 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, pp. 249–268. Springer (2017) Dimovski, A.S., Wasowski, A.: 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, pp. 249–268. Springer (2017)
25.
Zurück zum Zitat Dimovski, A.S., Wasowski, A.: 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 (2017) Dimovski, A.S., Wasowski, A.: 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 (2017)
26.
Zurück zum Zitat Ebert, C., Jones, C.: Embedded software: facts, figures, and future. IEEE Comput. 42(4), 42–52 (2009)CrossRef Ebert, C., Jones, C.: Embedded software: facts, figures, and future. IEEE Comput. 42(4), 42–52 (2009)CrossRef
27.
Zurück zum Zitat Gazzillo, P., Grimm, R.: 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, pp. 323–334. ACM (2012) Gazzillo, P., Grimm, R.: 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, pp. 323–334. ACM (2012)
28.
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, volume 5051 of LNCS, 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, volume 5051 of LNCS, pp. 113–131. Springer (2008)
29.
Zurück zum Zitat Iosif-Lazar, A.F., Al-Sibahi, A.S., Dimovski, A.S., Savolainen, J.E., Sierszecki, K., Wasowski, A.: 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 (2015) Iosif-Lazar, A.F., Al-Sibahi, A.S., Dimovski, A.S., Savolainen, J.E., Sierszecki, K., Wasowski, A.: 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 (2015)
30.
Zurück zum Zitat Iosif-Lazar, A.F., Melo, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Effective analysis of c programs by rewriting variability. Program. J. 1(1), 1 (2017)CrossRef Iosif-Lazar, A.F., Melo, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Effective analysis of c programs by rewriting variability. Program. J. 1(1), 1 (2017)CrossRef
31.
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
32.
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 Conf. on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011. pp. 805–824 (2011)CrossRef 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 Conf. on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011. pp. 805–824 (2011)CrossRef
33.
Zurück zum Zitat Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983)CrossRef Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983)CrossRef
34.
Zurück zum Zitat Larsen, K.G., Nyman, U., Wasowski, A.: 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, pp. 64–79. Springer (2007)CrossRef Larsen, K.G., Nyman, U., Wasowski, A.: 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, pp. 64–79. Springer (2007)CrossRef
35.
Zurück zum Zitat Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS ’88), pp. 203–210. IEEE Computer Society (1988) Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS ’88), pp. 203–210. IEEE Computer Society (1988)
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)MathSciNetCrossRef 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)MathSciNetCrossRef
37.
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
38.
Zurück zum Zitat Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)CrossRef Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)CrossRef
39.
Zurück zum Zitat Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Comput. Log. 9(1), 1 (2007)MathSciNetCrossRef Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Comput. Log. 9(1), 1 (2007)MathSciNetCrossRef
40.
Zurück zum Zitat Shoham, S., Grumberg, O.: Compositional verification and 3-valued abstractions join forces. Inf. Comput. 208(2), 178–202 (2010)MathSciNetCrossRef Shoham, S., Grumberg, O.: Compositional verification and 3-valued abstractions join forces. Inf. Comput. 208(2), 178–202 (2010)MathSciNetCrossRef
41.
Zurück zum Zitat ter Beek, M.H., de Vink, E.P., Willemse, T.A.C.: Family-based model checking with mcrl2. In: Fundamental Approaches to Software Engineering—20th International Conference, FASE 2017, Proceedings, volume 10202 of LNCS, pp. 387–405 (2017) ter Beek, M.H., de Vink, E.P., Willemse, T.A.C.: Family-based model checking with mcrl2. In: Fundamental Approaches to Software Engineering—20th International Conference, FASE 2017, Proceedings, volume 10202 of LNCS, pp. 387–405 (2017)
42.
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)MathSciNetCrossRef 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)MathSciNetCrossRef
43.
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
44.
Zurück zum Zitat von Rhein, A., Thüm, T., Schaefer, I., Liebig, J., Apel, S.: Variability encoding: from compile-time to load-time variability. J. Log. Algebraic Methods Program. 85(1), 125–145 (2016)MathSciNetCrossRef von Rhein, A., Thüm, T., Schaefer, I., Liebig, J., Apel, S.: Variability encoding: from compile-time to load-time variability. J. Log. Algebraic Methods Program. 85(1), 125–145 (2016)MathSciNetCrossRef
Metadaten
Titel
family-based model checking using variability abstractions and modal transition systems
verfasst von
Aleksandar S. Dimovski
Publikationsdatum
09.08.2019
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-019-00528-0