Advertisement

Frontiers of Computer Science

, Volume 12, Issue 2, pp 264–279 | Cite as

Efficient software product-line model checking using induction and a SAT solver

  • Fei He
  • Yuan Gao
  • Liangze Yin
Research Article
  • 32 Downloads

Abstract

Software product line (SPL) engineering is increasingly being adopted in safety-critical systems. It is highly desirable to rigorously show that these systems are designed correctly. However, formal analysis for SPLs is more difficult than for single systems because an SPL may contain a large number of individual systems. In this paper, we propose an efficient model-checking technique for SPLs using induction and a SAT (Boolean satisfiability problem) solver. We show how an induction-based verification method can be adapted to the SPLs, with the help of a SAT solver. To combat the state space explosion problem, a novel technique that exploits the distinguishing characteristics of SPLs, called feature cube enlargement, is proposed to reduce the verification efforts. The incremental SAT mechanism is applied to further improve the efficiency. The correctness of our technique is proved. Experimental results show dramatic improvement of our technique over the existing binary decision diagram (BDD)-based techniques.

Keywords

software product line model checking satisfiability 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Notes

Acknowledgements

This work was supported in part by the National Basic Research Program of China (973 Program) (2010CB328003), the National Natural Science Foundation of China (Grant Nos. 61672310, 61272001, 60903030, 91218302), and the Chinese National Key Technology R&D Program (SQ2012BAJY4052).

Supplementary material

11704_2016_6048_MOESM1_ESM.ppt (160 kb)
Supplementary material, approximately 228 KB.

References

  1. 1.
    Clements P, Northrop L. Software Product Lines: Practices and Patterns. Boston, MA: Addison-Wesley, 2002Google Scholar
  2. 2.
    Pohl K, Böckle G, Van Der Linden F. Software Product Line Engineering. Berlin: Springer, 2005CrossRefzbMATHGoogle Scholar
  3. 3.
    Thüm T, Apel S, Kästner C, Schaefer I, Saake G. A classification and survey of analysis strategies for software product lines. ACM Computing Surveys, 2014, 47(1): 6CrossRefGoogle Scholar
  4. 4.
    Galster M, Weyns D, Tofan D, Michalik B, Avgeriou P. Variability in software systems — a systematic literature review. IEEE Transactions on Software Engineering, 2014, 40(3): 282–306CrossRefGoogle Scholar
  5. 5.
    Dordowsky F, Hipp W. Adopting software product line principles to manage software variants in a complex avionics system. In: Proceedings of the 13th International Software Product Line Conference. 2009, 265–274Google Scholar
  6. 6.
    Hutchesson S, McDermid J. Development of high-integrity software product lines using model transformation. In: Proceedings of the 29th International Conference on Computer Safety, Reliability, and Security. 2010, 389–401CrossRefGoogle Scholar
  7. 7.
    Polzer A, Kowalewski S, Botterweck G. Applying software product line techniques in model-based embedded systems engineering. In: Proceedings of International Workshop on Model-Based Methodologies for Pervasive and Embedded Software. 2009, 2–10Google Scholar
  8. 8.
    Van Ommering R. Building product populations with software components. In: Proceedings of the 24th International Conference on Software Engineering. 2002, 255–265Google Scholar
  9. 9.
    Braga R T V, Junior O T, Branco K R C, Neris L D O, Lee J. Adapting a software product line engineering process for certifying safety critical embedded systems. In: Proceedings of the 31st International Conference on Computer Safety, Reliability, and Security. 2012, 352–363Google Scholar
  10. 10.
    Clarke E M, Grumberg O, Peled D. Model Checking. Cambridge: MIT press, 1999Google Scholar
  11. 11.
    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. 2010, 335–344Google Scholar
  12. 12.
    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. 2011, 321–330Google Scholar
  13. 13.
    Gruler A, Leucker M, Scheidemann K. Modeling and model checking software product lines. In: Proceedings of the International Conference on Formal Methods for Open Object-Based Distributed Systems. 2008, 113–131CrossRefGoogle Scholar
  14. 14.
    Lauenroth K, Pohl K, Toehning S. Model checking of domain artifacts in product line engineering. In: Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering. 2009, 269–280Google Scholar
  15. 15.
    Beek M H T, Mazzanti F, Sulova A. VMC: a tool for product variability analysis. In: Giannakopoulou D, Méry D, eds. FM 2012: Formal Methods. Berlin: Springer-Verlag, 2012, 450–454Google Scholar
  16. 16.
    Sabouri H, Khosravi R. Efficient verification of evolving software product lines. In: Proceedings of the International Conference on Fundamentals of Software Engineering. 2012, 351–358CrossRefGoogle Scholar
  17. 17.
    Cordy M, Schobbens P Y, Heymans P, Legay A. Beyond boolean product-line model checking: dealing with feature attributes and multifeatures. In: Proceedings of the International Conference on Software Engineering. 2013, 472–481Google Scholar
  18. 18.
    Cordy M, Classen A, Heymans P, Schobbens P Y, Legay A. ProVe-Lines: a product line of verifiers for software product lines. In: Proceedings of the 17th International Software Product Line Conference co-located workshops. 2013, 141–146CrossRefGoogle Scholar
  19. 19.
    Tartler R, Lohmann D, Dietrich C, Egger C, Sincero J. Configuration coverage in the analysis of large-scale system software. In: Proceedings of the 6th Workshop on Programming Languages and Operating Systems. 2011Google Scholar
  20. 20.
    Classen A, Cordy M, Heymans P, Legay A, Schobbens P Y. Formal semantics, modular specification, and symbolic verification of productline behaviour. Science of Computer Programming, 2014, 80: 416–439CrossRefGoogle Scholar
  21. 21.
    Prasad M R, Biere A, Gupta A. A survey of recent advances in SATbased formal verification. International Journal on Software Tools for Technology Transfer, 2005, 7(2): 156–173CrossRefGoogle Scholar
  22. 22.
    Biere A, Cimatti A, Clarke E M, Zhu Y. Symbolic model checking without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems. 1999, 193–207Google Scholar
  23. 23.
    Shtrichman O. Tuning SAT checkers for bounded model checking. In: Proceedings of the 12th International Conference on Computer Aided Verification. 2000, 480–494CrossRefGoogle Scholar
  24. 24.
    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 International Conference on Software Engineering. 2012, 672–682Google Scholar
  25. 25.
    Apel S, Speidel H, Wendler P, Rheinv A, Beyer D. Detection of feature interactions using feature-aware verification. In: Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering. 2011, 372–375Google Scholar
  26. 26.
    Apel S, Rhein A V, Wendler P, Größlinger A, Beyer D. Strategies for product-line verification: case studies and experiments. In: Proceedings of the International Conference on Software Engineering. 2013, 482–491Google Scholar
  27. 27.
    Clarke E, Kroening D, Lerda F. A tool for checking ANSI-C programs. In: Jensen K, Podelski A, eds. Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer-Verlag, 2004, 168–176Google Scholar
  28. 28.
    Eén N, Sörensson N. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 2003, 89(4): 543–560CrossRefzbMATHGoogle Scholar
  29. 29.
    Eén N, Sörensson N. An extensible SAT-solver. In: Giunchiglia E, Tacchella A, eds. Theory and Applications of Satisfiability Testing. Berlin: Springer-Verlag, 2004, 502–518CrossRefGoogle Scholar
  30. 30.
    Biere A. PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation, 2008, 4(2–4): 75–97zbMATHGoogle Scholar
  31. 31.
    Clarke E, Kroening D, Ouaknine J, Strichman O. Completeness and complexity of bounded model checking. Lecture Notes in Computer Science, 2004, 2937(4): 85–96MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    McMillan K L. Applying SAT methods in unbounded symbolic model checking. In: Proceedings of the International Conference on Computer Aided Verification. 2002, 250–264CrossRefGoogle Scholar
  33. 33.
    Sheeran M, Singh S, Stålmarck G. Checking safety properties using induction and a SAT-solver. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design. 2000, 127–144CrossRefGoogle Scholar
  34. 34.
    McMillan K L. Interpolation and sat-based model checking. Lecture Notes in Computer Science, 2003, 2725: 1–13MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Plath M, Ryan M. Feature integration using a feature construct. Science of Computer Programming, 2001, 41(1): 53–84CrossRefzbMATHGoogle Scholar
  36. 36.
    McMillan K L. Symbolic Model Checking. Boston, MA: Springer US, 1993CrossRefzbMATHGoogle Scholar
  37. 37.
    Mannion M. Using first-order logic for product line model validation. In: Proceedings of the 2nd International Conference on Software Product Lines. 2002, 176–187CrossRefGoogle Scholar
  38. 38.
    Batory D. Feature models, grammars, and propositional formulas. In: Proceedings of the 9th International Software Product Lines Conference. 2005, 7–20CrossRefGoogle Scholar
  39. 39.
    Mendonca M, Wasowski A, Czarnecki K. SAT-based analysis of feature models is easy. In: Proceedings of the 13th International Software Product Line Conference. 2009, 231–240Google Scholar
  40. 40.
    Biere A, Artho C, Schuppan V. Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science, 2002, 66(2): 160–177CrossRefGoogle Scholar
  41. 41.
    Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2: an opensource tool for symbolic model checking. In: Proceedings of the International Conference on Computer Aided Verification. 2002, 359–364CrossRefGoogle Scholar
  42. 42.
    Hall R J. Fundamental nonmodularity in electronic mail. Automated Software Engineering, 2005, 12(1): 41–79CrossRefGoogle Scholar
  43. 43.
    Classen A. Modelling with FTS: a collection of illustrative examples. Technical Report P-CS-TR SPLMC-00000001. 2010Google Scholar
  44. 44.
    Fantechi A, Gnesi S. Formal modeling for product families engineering. In: Proceedings of the 12th International Conference on Software Product Line. 2008, 193–202Google Scholar
  45. 45.
    Ellenbogen K A, Wood M A. Cardiac Pacing and ICDs. New York: John Wiley & Sons, 2008Google Scholar
  46. 46.
    Classen A, Cordy M, Heymans P, Legay A, Schobbens P Y. Model checking software product lines with SNIP. International Journal on Software Tools for Technology Transfer, 2012, 14(5): 589–612CrossRefGoogle Scholar
  47. 47.
    Asirelli P, ter Beek M H, Fantechi A, Gnesi S. A compositional framework to derive product line behavioural descriptions. In: Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. 2012, 146–161Google Scholar
  48. 48.
    Gupta A, Yang Z, Ashar P, Gupta A. SAT-based image computation with application in reachability analysis. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design. 2000, 391–408CrossRefGoogle Scholar
  49. 49.
    Ganai M K, Gupta A, Ashar P. Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In: Proceedings of IEEE/ACMInternational Conference on Computer-aided design. 2004, 510–517Google Scholar
  50. 50.
    Schobbens P, Heymans P, Trigaux J C. Feature diagrams: a survey and a formal semantics. In: Proceedings of the 14th IEEE International Conference on Requirements Engineering. 2006, 139–148CrossRefGoogle Scholar

Copyright information

© Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Tsinghua National Laboratory for Information Science and Technology (TNList)Tsinghua UniversityBeijingChina
  2. 2.Key Laboratory for Information System SecurityMinistry of EducationBeijingChina
  3. 3.School of SoftwareTsinghua UniversityBeijingChina
  4. 4.Department of Computer Science and TechnologyNational University of Defense TechnologyChangshaChina

Personalised recommendations