Advertisement

Variability-Specific Abstraction Refinement for Family-Based Model Checking

  • Aleksandar S. DimovskiEmail author
  • Andrzej Wąsowski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10202)

Abstract

Variational systems are ubiquitous in many application areas today. They use features to control presence and absence of system functionality. One challenge in the development of variational systems is their formal analysis and verification. Researchers have addressed this problem by designing aggregate so-called family-based verification algorithms. Family-based model checking allows simultaneous verification of all variants of a system family (variational system) in a single run by exploiting the commonalities between the variants. Yet, the computational cost of family-based model checking still greatly depends on the number of variants. In order to make it computationally cheaper, we can use variability abstractions for deriving abstract family-based model checking, where the variational model of a system family is replaced with an abstract (smaller) version of it which preserves the satisfaction of LTL properties. The variability abstractions can be combined with different partitionings of the set of variants to infer various verification scenarios for the variational model. However, manually finding an optimal verification scenario is hard since it requires a good knowledge of the family and property, while the number of possible scenarios is very large.

In this work, we present an automatic iterative abstraction refinement procedure for family-based model checking. We use Craig interpolation to refine abstract variational models based on the obtained spurious counterexamples (traces). The refinement procedure works until a genuine counterexample is found or the property satisfaction is shown for all variants in the family. We illustrate the practicality of this approach for several variational benchmark models.

Keywords

Model Check Feature Expression Galois Connection Initial Abstraction Software Product Line Engineer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  2. 2.
    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. Algebr. Meth. Program. 85(2), 287–315 (2016). http://dx.doi.org/10.1016/j.jlamp.2015.09.004 MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    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 2013, pp. 355–364 (2013)Google Scholar
  4. 4.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). doi: 10.1007/10722167_15 CrossRefGoogle Scholar
  5. 5.
    Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Meth. Syst. Des. 25(2–3), 105–127 (2004). http://dx.doi.org/10.1023/B:FORM.0000040025.89719.f3 CrossRefzbMATHGoogle Scholar
  6. 6.
    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). http://dx.doi.org/10.1016/j.scico.2010.10.005 CrossRefGoogle Scholar
  7. 7.
    Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.: Model checking software product lines with SNIP. STTT 14(5), 589–612 (2012). http://dx.doi.org/10.1007/s10009-012-0234-1 CrossRefGoogle Scholar
  8. 8.
    Classen, A., Cordy, M., Schobbens, P., Heymans, P., Legay, A., Raskin, J.: 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). http://doi.ieeecomputersociety.org/10.1109/TSE.2012.86 CrossRefGoogle Scholar
  9. 9.
    Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley, Reading (2001)Google Scholar
  10. 10.
    Cordy, M., Heymans, P., Legay, A., Schobbens, P., Dawagne, B., Leucker, M.: Counterexample guided abstraction refinement of product-line behavioural models. In: Cheung, S., Orso, A., Storey, M.D. (eds.) Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE-22), pp. 190–201. ACM (2014). http://doi.acm.org/10.1145/2635868.2635919
  11. 11.
    Dimovski, A.S.: Program verification using symbolic game semantics. Theor. Comput. Sci. 560, 364–379 (2014). http://dx.doi.org/10.1016/j.tcs.2014.01.016 MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Dimovski, A.S.: Symbolic game semantics for model checking program families. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 19–37. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-32582-8_2 CrossRefGoogle Scholar
  13. 13.
    Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wąsowski, A.: Family-based model checking without a family-based model checker. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 282–299. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-23404-5_18 CrossRefGoogle Scholar
  14. 14.
    Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wasowski, A.: Efficient family-based model checking via variability abstractions. STTT 1–19 (2016). doi: 10.1007/s10009-016-0425-2
  15. 15.
    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). http://dx.doi.org/10.4230/LIPIcs.ECOOP.2015.247
  16. 16.
    Dimovski, A.S., Brabrand, C., Wąsowski, A.: Finding suitable variability abstractions for family-based analysis. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 217–234. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-48989-6_14 CrossRefGoogle Scholar
  17. 17.
    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 2012, Beijing, China, 11–16 June 2012, pp. 323–334. ACM (2012). http://doi.acm.org/10.1145/2254064.2254103
  18. 18.
    Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, pp. 232–244. ACM (2004). http://doi.acm.org/10.1145/964001.964021
  19. 19.
    Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2004)Google Scholar
  20. 20.
    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). http://dx.doi.org/10.1109/ASE.2015.84
  21. 21.
    Iosif-Lazar, A.F., Melo, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Effective analysis of c programs by rewriting variability. In: The Art, Science, and Engineering of Programming, Programming 2017 (2017)Google Scholar
  22. 22.
    Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Peterson, A.S.: Feature-oriented domain analysis (FODA) feasibility study. Technical report, Carnegie-Mellon University Software Engineering Institute, November 1990Google Scholar
  23. 23.
    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)CrossRefGoogle Scholar
  24. 24.
    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, pp. 805–824 (2011). http://doi.acm.org/10.1145/2048066.2048128
  25. 25.
    Kramer, J., Magee, J., Sloman, M., Lister, A.: Conic: an integrated approach to distributed computer control systems. IEE Proc. 130(1), 1–10 (1983)CrossRefGoogle Scholar
  26. 26.
    Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71316-6_6 CrossRefGoogle Scholar
  27. 27.
    McMillan, K.L.: Applications of craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1–12. Springer, Heidelberg (2005). doi: 10.1007/978-3-540-31980-1_1 CrossRefGoogle Scholar
  28. 28.
    Midtgaard, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program. 105, 145–170 (2015). http://dx.doi.org/10.1016/j.scico.2015.04.005 CrossRefGoogle Scholar
  29. 29.
    von Rhein, A., Thüm, T., Schaefer, I., Liebig, J., Apel, S.: Variability encoding: from compile-time to load-time variability. J. Log. Algebr. Meth. Program. 85(1), 125–145 (2016). http://dx.doi.org/10.1016/j.jlamp.2015.06.007 MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    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). http://doi.acm.org/10.1145/2580950 CrossRefGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany 2017

Authors and Affiliations

  1. 1.Computer ScienceIT University of CopenhagenCopenhagen SDenmark

Personalised recommendations