|
|
Efficient software product-line model checking using induction and a SAT solver |
Fei HE1,2,3( ), Yuan GAO1,2,3, Liangze YIN4 |
1. Tsinghua National Laboratory for Information Science and Technology (TNList), Tsinghua University, Beijing 100084, China 2. Key Laboratory for Information System Security, Ministry of Education, Beijing 100084, China 3. School of Software, Tsinghua University, Beijing 100084, China 4. Department of Computer Science and Technology, National University of Defense Technology, Changsha 410073, China |
|
|
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
|
Corresponding Author(s):
Fei HE
|
Just Accepted Date: 19 December 2016
Online First Date: 06 March 2018
Issue Date: 26 March 2018
|
|
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
https://doi.org/10.1007/3-540-28901-1
|
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
https://doi.org/10.1145/2580950
|
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
https://doi.org/10.1109/TSE.2013.56
|
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
https://doi.org/10.1007/978-3-642-15651-9_29
|
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
https://doi.org/10.1109/MOMPES.2009.5069132
|
8 |
Van Ommering R. Building product populations with software components. In: Proceedings of the 24th International Conference on Software Engineering. 2002, 255–265
https://doi.org/10.1145/581372.581373
|
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
https://doi.org/10.1007/978-3-642-33678-2_30
|
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
https://doi.org/10.1145/1806799.1806850
|
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
https://doi.org/10.1145/1985793.1985838
|
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
https://doi.org/10.1007/978-3-540-68863-1_8
|
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
https://doi.org/10.1109/ASE.2009.16
|
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
https://doi.org/10.1007/978-3-642-32759-9_36
|
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
https://doi.org/10.1007/978-3-642-29320-7_24
|
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
https://doi.org/10.1109/ICSE.2013.6606593
|
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
https://doi.org/10.1145/2499777.2499781
|
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
https://doi.org/10.1145/2039239.2039242
|
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
https://doi.org/10.1016/j.scico.2013.09.019
|
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
https://doi.org/10.1007/s10009-004-0183-4
|
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
https://doi.org/10.21236/ADA360973
|
23 |
Shtrichman O. Tuning SAT checkers for bounded model checking. In: Proceedings of the 12th International Conference on Computer Aided Verification. 2000, 480–494
https://doi.org/10.1007/10722167_36
|
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
https://doi.org/10.1109/ICSE.2012.6227150
|
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
https://doi.org/10.1109/ICSE.2013.6606594
|
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
https://doi.org/10.1007/978-3-540-24730-2_15
|
28 |
Eén N, Sörensson N. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 2003, 89(4): 543–560
https://doi.org/10.1016/S1571-0661(05)82542-3
|
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
https://doi.org/10.1007/978-3-540-24605-3_37
|
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
https://doi.org/10.1007/978-3-540-24622-0_9
|
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
https://doi.org/10.1007/3-540-45657-0_19
|
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
https://doi.org/10.1007/3-540-40922-X_8
|
34 |
McMillan K L. Interpolation and sat-based model checking. Lecture Notes in Computer Science, 2003, 2725: 1–13
https://doi.org/10.1007/978-3-540-45069-6_1
|
35 |
Plath M, Ryan M. Feature integration using a feature construct. Science of Computer Programming, 2001, 41(1): 53–84
https://doi.org/10.1016/S0167-6423(00)00018-6
|
36 |
McMillan K L. Symbolic Model Checking. Boston, MA: Springer US, 1993
https://doi.org/10.1007/978-1-4615-3190-6
|
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
https://doi.org/10.1007/3-540-45652-X_11
|
38 |
Batory D. Feature models, grammars, and propositional formulas. In: Proceedings of the 9th International Software Product Lines Conference. 2005, 7–20
https://doi.org/10.1007/11554844_3
|
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
https://doi.org/10.1016/S1571-0661(04)80410-9
|
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
https://doi.org/10.1007/3-540-45657-0_29
|
42 |
Hall R J. Fundamental nonmodularity in electronic mail. Automated Software Engineering, 2005, 12(1): 41–79
https://doi.org/10.1023/B:AUSE.0000049208.84702.84
|
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
https://doi.org/10.1109/SPLC.2008.45
|
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
https://doi.org/10.1007/s10009-012-0234-1
|
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
https://doi.org/10.1007/978-3-642-34026-0_12
|
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
https://doi.org/10.1007/3-540-40922-X_22
|
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
https://doi.org/10.1109/ICCAD.2004.1382631
|
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
https://doi.org/10.1109/RE.2006.23
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|