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

doi:10.1007/s11704-016-6048-7

Front. Comput. Sci.

2018, Vol. 12

Issue (2) : 264-279 https://doi.org/10.1007/s11704-016-6048-7

RESEARCH ARTICLE

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

Fei HE^1,^2,³(

), Yuan GAO^1,^2,³, Liangze YIN⁴

¹. Tsinghua National Laboratory for Information Science and Technology (TNList), Tsinghua University, Beijing 100084, China
². Key Laboratory for Information System Security, Ministry of Education, Beijing 100084, China
³. School of Software, Tsinghua University, Beijing 100084, China
⁴. Department of Computer Science and Technology, National University of Defense Technology, Changsha 410073, China

Download: PDF(541 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Cite this article:

Fei HE,Yuan GAO,Liangze YIN. Efficient software product-line model checking using induction and a SAT solver[J]. Front. Comput. Sci., 2018, 12(2): 264-279.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-016-6048-7
https://academic.hep.com.cn/fcs/EN/Y2018/V12/I2/264

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

[1]

Download

[1]	Yongping WANG, Daoyun XU. Properties of the satisfiability threshold of the strictly d-regular random (3, 2s)-SAT problem[J]. Front. Comput. Sci., 2020, 14(6): 146404-.
[2]	Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[3]	Yi CHU, Chuan LUO, Shaowei CAI, Haihang YOU. Empirical investigation of stochastic local search for maximum satisfiability[J]. Front. Comput. Sci., 2019, 13(1): 86-98.
[4]	Kazuhiro OGATA. A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions[J]. Front. Comput. Sci., 2019, 13(1): 51-72.
[5]	Chen LUO, Fei HE. SMT-based query tracking for differentially private data analytics systems[J]. Front. Comput. Sci., 2018, 12(6): 1192-1207.
[6]	Anil Kumar KARNA, Yuting CHEN, Haibo YU, Hao ZHONG, Jianjun ZHAO. The role of model checking in software engineering[J]. Front. Comput. Sci., 2018, 12(4): 642-668.
[7]	Yu ZHOU, Nvqi ZHOU, Tingting HAN, Jiayi GU, Weigang WU. Probabilistic verification of hierarchical leader election protocol in dynamic systems[J]. Front. Comput. Sci., 2018, 12(4): 763-776.
[8]	Sedigheh KHOSHNEVIS, Fereidoon SHAMS. Automating identification of services and their variability for product lines using NSGA-II[J]. Front. Comput. Sci., 2017, 11(3): 444-464.
[9]	Yang BO, Chunhe XIA, Zhigang ZHANG, Xinzheng LU. On the satisfiability of authorization requirements in business process[J]. Front. Comput. Sci., 2017, 11(3): 528-540.
[10]	Laixiang SHAN,Xiaomin DU,Zheng QIN. Efficient approach of translating LTL formulae into Büchi automata[J]. Front. Comput. Sci., 2015, 9(4): 511-523.
[11]	Luxi CHEN,Linpeng HUANG,Chen LI,Tao ZAN. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.
[12]	Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[13]	Savas KONUR. A survey on temporal logics for specifying and verifying real-time systems[J]. Front. Comput. Sci., 2013, 7(3): 370-403.
[14]	Anh Tuan LUU, Jun SUN, Yang LIU, Jin Song DONG, Xiaohong LI, Thanh Tho QUAN. SeVe: automatic tool for verification of security protocols[J]. Front Comput Sci, 2012, 6(1): 57-75.
[15]	Conghua ZHOU, Bo SUN, Zhifeng LIU. Abstraction for model checking multi-agent systems[J]. Front Comput Sci Chin, 2011, 5(1): 14-25.

Viewed

Full text

Abstract

Cited

Shared

Discussed