User menu

Accès à distance ? S'identifier sur le proxy UCLouvain

Counterexample Guided Abstraction Refinement of Product-Line Behavioural Models

Primary tabs

Cordy, Maxime Heymans, Patrick Legay, Axel [UCL] Schobbens, Pierre-Yves Dawagne, Bruno Leucker, Martin

The model-checking problem for Software Products Lines (SPLs) is harder than for single systems: variability constitutes a new source of complexity that exacerbates the state-explosion problem. Abstraction techniques have successfully alleviated state explosion in single-system models. However, they need to be adapted to SPLs, to take into account the set of variants that produce a counterexample. In this paper, we apply CEGAR (Counterexample-Guided Abstraction Refinement) and we design new forms of abstraction specifically for SPLs. We carry out experiments to evaluate the efficiency of our new abstractions. The results show that our abstractions, combined with an appropriate refinement strategy, hold the potential to achieve large reductions in verification time, although they sometimes perform worse. We discuss in which cases a given abstraction should be used.

Document type Communication à un colloque (Conference Paper) – Présentation orale avec comité de sélection
Publication date 2014
Language Anglais
Conference "FSE 2014 : International Symposium on Foundations of Software Engineering", Hong Kong, China (11/2014)
Host document "Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering - FSE 2014" (ISBN : 9781450330565)
Publisher ACM Press (New York, New York, USA)
Publication status Publié
Affiliation UCL - SST/ICTM/INGI - Pôle en ingénierie informatique
Links
  1. P.-Y. Schobbens, P. Heymans, J.-C. Trigaux, and Y. Bontemps. Feature Diagrams: A Survey and A Formal Semantics. In RE’06, pages 139–148, 2006.
  2. H. Post and C. Sinz. Configuration lifting: Verification meets software configuration. In ASE’08, pages 347–350. IEEE CS, 2008.
  3. A. Pnueli. The temporal logic of programs. In FOCS’77, pages 46–57, 1977.
  4. M. Plath and M. Ryan. Feature integration using a feature construct. SCP, 41(1):53–84, 2001.
  5. J. Morse, L. Cordeiro, D. Nicole, and B. Fischer. Handling unbounded loops with esbmc 1.20 - (competition contribution). In TACAS, pages 619–622, 2013.
  6. R. Milner. An algebraic definition of simulation between programs. Technical report, Stanford University, Stanford, CA, USA, 1971.
  7. J. Liebig, A. von Rhein, C. Kästner, S. Apel, J. Dörre, and C. Lengauer. Scalable analysis of variable software. In ESEC/SIGSOFT FSE ’11, pages 81–91, 2013.
  8. J. Kramer, J. Magee, M. Sloman, and A. Lister. Conic: an integrated approach to distributed computer control systems. Computers and Digital Techniques, IEE Proceedings E, 130(1):1–10, 1983.
  9. K. Kang, S. Cohen, J. Hess, W. Novak, and S. Peterson. Feature-oriented domain analysis (FODA) feasibility study. Technical Report CMU/SEI-90-TR-21, 1990.
  10. G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004.
  11. A. Gruler, M. Leucker, and K. Scheidemann. Modeling and model checking software product lines. In FMOODS’08, pages 113–131. Springer, 2008.
  12. S. Graf and H. Sa¨ıdi. Construction of abstract state graphs with pvs. In Proceedings of the 9th International Conference on Computer Aided Verification, CAV ’97, pages 72–83, London, UK, UK, 1997. Springer-Verlag.
  13. D. Fischbein, S. Uchitel, and V. Braberman. A foundation for behavioural conformance in software product line architectures. In ROSATEA’06, ISSTA 2006 workshop, pages 39–48. ACM Press, 2006.
  14. S. Falke, F. Merz, and C. Sinz. The bounded model checker llbmc. In ASE ’13, pages 706–709, 2013.
  15. W. Craig. Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. The Journal of Symbolic Logic, 22(3):269–285, 1957.
  16. M. Cordy, P.-Y. Schobbens, P. Heymans, and A. Legay. Provelines: A product-line of verifiers for software product lines. In SPLC’13, pages 141–146. ACM, 2013.
  17. M. Cordy, A. Classen, G. Perrouin, P. Heymans, P.-Y. Schobbens, and A. Legay. Simulation-based abstractions for software product-line model checking. In ICSE’12, pages 672–682. IEEE, 2012.
  18. M. Cordy, A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. Managing evolution in software product lines : A model-checking perspective. In VaMoS’12, pages 183–191. ACM, 2012.
  19. Consultative Committee for Space Data Systems (CCSDS). CCSDS File Delivery Protocol (CFDP): Blue Book, Issue 4. NASA, 2007.
  20. P. C. Clements and L. Northrop. Software Product Lines: Practices and Patterns. SEI Series in Software Engineering. Addison-Wesley, August 2001.
  21. A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay, and J.-F. Raskin. Model checking lots of systems: efficient verification of temporal properties in software product lines. In ICSE’10, pages 335–344. ACM, 2010.
  22. A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. Symbolic model checking of software product lines. In ICSE’11, pages 321–330. ACM, 2011.
  23. A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. cois Raskin. Featured transition systems: Foundations for verifying variability-intensive systems and their application to LTL model checking. Transactions on Software Engineering, pages 1069–1089, 2013.
  24. A. Classen, M. Cordy, P. Heymans, P.-Y. Schobbens, and A. Legay. Snip: An efficient model checker for software product lines. Technical report, University of Namur (FUNDP), 2011.
  25. A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens. Model checking software product lines with SNIP. STTT, 14(5):589–612, 2012.
  26. E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. Predicate abstraction of ansi-c programs using sat. Form. Methods Syst. Des., 25(2-3):105–127, Sept. 2004.
  27. E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
  28. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In E. Emerson and A. Sistla, editors, Computer Aided Verification, volume 1855 of LNCS, pages 154–169. Springer Berlin / Heidelberg, 2000.
  29. M. Chechik, B. Devereux, and A. Gurfinkel. Model-checking infinite state-space systems with fine-grained abstractions using spin. In SPIN ’01, pages 16–36, 2001.
  30. G. Bruns and P. Godefroid. Model checking with multi-valued logics. In ICALP ’04, pages 281–293, 2004.
  31. Q. Boucher, A. Classen, P. Heymans, A. Bourdoux, and L. Demonceau. Tag and prune: A pragmatic approach to software product line implementation. In ASE’10, pages 333–336. ACM, 2010.
  32. D. Beyer and M. E. Keremoglu. Cpachecker: A tool for configurable software verification. In CAV ’11, pages 184–190, 2011.
  33. D. Beyer. Second competition on software verification - (summary of sv-comp 2013). In TACAS ’13, pages 594–609, 2013.
  34. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2007.
  35. P. Asirelli, M. H. ter Beek, A. Fantechi, and S. Gnesi. Formal description of variability in product families. In SPLC’11, pages 130–139. Springer-Verlag, 2011.
  36. S. Apel, A. von Rhein, P. Wendler, A. Größlinger, and D. Beyer. Strategies for product-line verification: case studies and experiments. In ICSE’13, pages 482–491, 2013.
  37. S. Apel, H. Speidel, P. Wendler, A. von Rhein, and D. Beyer. Feature-interaction detection using feature-aware verification. In ASE’11, pages 372–375. IEEE, 2011.
  38. A. Albarghouthi, Y. Li, A. Gurfinkel, and M. Chechik. Ufo: A framework for abstraction- and interpolation-based software verification. In CAV, pages 672–678, 2012.
Bibliographic reference Cordy, Maxime ; Heymans, Patrick ; Legay, Axel ; Schobbens, Pierre-Yves ; Dawagne, Bruno ; et. al. Counterexample Guided Abstraction Refinement of Product-Line Behavioural Models.FSE 2014 : International Symposium on Foundations of Software Engineering (Hong Kong, China, 11/2014). In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering - FSE 2014, ACM Press : New York, New York, USA2014
Permanent URL https://hdl.handle.net/2078.1/210623