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

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

References

[1] Clements P, Northrop L. Software Product Lines: Practices and Patterns. Boston, MA: Addison-Wesley, 2002

[2] Pohl K, Böckle G, Van Der Linden F. Software Product Line Engineering. Berlin: Springer, 2005

[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): 6

[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–306

[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–274

[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–401

[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–10

[8] Van Ommering R. Building product populations with software components. In: Proceedings of the 24th International Conference on Software Engineering. 2002, 255–265

[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–363

[10] Clarke E M, Grumberg O, Peled D. Model Checking. Cambridge: MIT press, 1999

[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–344

[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–330

[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–131

[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–280

[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–454

[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–358

[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–481

[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–146

[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. 2011

[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–439

[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–173

[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–207

[23] Shtrichman O. Tuning SAT checkers for bounded model checking. In: Proceedings of the 12th International Conference on Computer Aided Verification. 2000, 480–494

[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–682

[25] Apel S, Speidel H, Wendler P, Rhein v 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–375

[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–491

[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–176

[28] Eén N, Sörensson N. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 2003, 89(4): 543–560

[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–518

[30] Biere A. PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation, 2008, 4(2–4): 75–97

[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–96

[32] McMillan K L. Applying SAT methods in unbounded symbolic model checking. In: Proceedings of the International Conference on Computer Aided Verification. 2002, 250–264

[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–144

[34] McMillan K L. Interpolation and sat-based model checking. Lecture Notes in Computer Science, 2003, 2725: 1–13

[35] Plath M, Ryan M. Feature integration using a feature construct. Science of Computer Programming, 2001, 41(1): 53–84

[36] McMillan K L. Symbolic Model Checking. Boston, MA: Springer US, 1993

[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–187

[38] Batory D. Feature models, grammars, and propositional formulas. In: Proceedings of the 9th International Software Product Lines Conference. 2005, 7–20

[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–240

[40] Biere A, Artho C, Schuppan V. Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science, 2002, 66(2): 160–177

[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–364

[42] Hall R J. Fundamental nonmodularity in electronic mail. Automated Software Engineering, 2005, 12(1): 41–79

[43] Classen A. Modelling with FTS: a collection of illustrative examples. Technical Report P-CS-TR SPLMC-00000001. 2010

[44] Fantechi A, Gnesi S. Formal modeling for product families engineering. In: Proceedings of the 12th International Conference on Software Product Line. 2008, 193–202

[45] Ellenbogen K A, Wood M A. Cardiac Pacing and ICDs. New York: John Wiley & Sons, 2008

[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–612

[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–161

[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–408

[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–517

[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–148

RIGHTS & PERMISSIONS

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