Verification of software product lines with delta-oriented slicing. (English) Zbl 1308.68038

Beckert, Bernhard (ed.) et al., Formal verification of object-oriented software. International conference, FoVeOOS 2010, Paris, France, June 28–30, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-18069-9/pbk). Lecture Notes in Computer Science 6528, 61-75 (2011).
Summary: Software product line (SPL) engineering is a well-known approach to develop industry-size adaptable software systems. SPL are often used in domains where high-quality software is desirable; the overwhelming product diversity, however, remains a challenge for assuring correctness. In this paper, we present delta-oriented slicing, an approach to reduce the deductive verification effort across an SPL where individual products are Java programs and their relations are described by deltas. On the specification side, we extend the delta language to deal with formal specifications. On the verification side, we combine proof slicing and similarity-guided proof reuse to ease the verification process.
For the entire collection see [Zbl 1204.68003].


68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)


JML; Chianti
Full Text: DOI Link


[1] Batory, D.S., Benavides, D., Ruiz-Cortés, A.: Automated analysis of feature models: Challenges ahead. Communications of the ACM 49(12) (2006)
[2] Batory, D.S., Börger, E.: Modularizing theorems for software product lines: The Jbook case study. Journal of Universal Computer Science 14(12) (2008)
[3] Batory, D.S., Sarvela, J.N., Rauschmayer, A.: Scaling step-wise refinement. IEEE Trans. Software Eng. 30(6), 355–371 (2004) · Zbl 05113893
[4] Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
[5] 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: 32nd International Conference on Software Engineering, ICSE 2010, Cape Town, South Africa, May 2-8. IEEE, Los Alamitos (2010) (to appear)
[6] Czarnecki, K., Pietroszek, K.: Verifying feature-based model templates against well-formedness OCL constraints. In: Conf. on Generative Programming and Component Engineering (GPCE) (2006)
[7] Delaware, B., Cook, W., Batory, D.: A Machine-Checked Model of Safe Composition. In: Foundations of Aspect-Oriented Languages (FOAL), pp. 31–35. ACM, New York (2009)
[8] Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley Longman, Amsterdam (2005) · Zbl 0865.68001
[9] Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Higher-Order and Symbolic Computation 13(4), 315–353 (2000) · Zbl 0972.68021
[10] Hutter, D.: Management of change in structured verification. In: Automated Software Engineering (ASE), p. 23 (2000)
[11] Klebanov, V.: Proof reuse. In: Beckert et al. [4]
[12] Lauenroth, K., Pohl, K., Toehning, S.: Model checking of domain artifacts in product line engineering. In: Automated Software Engineering (ASE), pp. 269–280. IEEE Computer Society, Los Alamitos (2009)
[13] Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006)
[14] Mannion, M.: Using First-Order Logic for Product Line Model Validation. In: Chastek, G.J. (ed.) SPLC 2002. LNCS, vol. 2379, pp. 176–187. Springer, Heidelberg (2002) · Zbl 1045.68543
[15] McGregor, J.D.: Testing a software product line. Technical Report CMU/SEI-2001-TR-022, Software Engineering Institute, Carnegie Mellon University (December 2001)
[16] Mossakowski, T.: Heterogeneous theories and the heterogeneous tool set. In: Kalfoglou, Y., Schorlemmer, W.M., Sheth, A.P., Staab, S., Uschold, M. (eds.) Semantic Interoperability and Integration. Dagstuhl Seminar Proceedings, vol. 04391, IBFI, Schloss Dagstuhl (2005)
[17] Muccini, H., van der Hoek, A.: Towards testing product line architectures. Electr. Notes Theor. Comput. Sci 82(6) (2003)
[18] Pohl, K., Böckle, G., van der Linden, F.: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer, Heidelberg (2005) · Zbl 1075.68575
[19] Ren, X., Shah, F., Tip, F., Ryder, B.G., Chesley, O.: Chianti: A tool for change impact analysis of Java programs. In: Vlissides, J.M., Schmidt, D.C. (eds.) Proceedings of the 19th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2004, Vancouver, BC, Canada, October 24-28, pp. 432–448. ACM, New York (2004)
[20] Roth, A.: Specification and Verification of Object-oriented Software Components. PhD thesis, Universität Karlsruhe (2006)
[21] Schaefer, I.: Variability modelling for model-driven development of software product lines. In: 4th Int. Workshop on Variability Modelling of Software-intensive Systems (VaMoS), Linz, Austria (January 2010)
[22] Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-Oriented Programming of Software Product Lines. In: Bosch, J., Lee, J. (eds.) SPLC 2010. LNCS, vol. 6287, pp. 77–91. Springer, Heidelberg (2010) · Zbl 05815058
[23] Schaefer, I., Worret, A., Poetzsch-Heffter, A.: A model-based framework for automated product derivation. In: Model-driven Approaches in Software Product Line Engineering (MAPLE 2009) (2009)
[24] Stenzel, K.: Verification of Java Card Programs. PhD thesis, Fakultät fur angewandte Informatik, University of Augsburg (2005)
[25] Tip, F.: A survey of program slicing techniques. Journal of Programming Languages 3(3) (1995)
[26] Wehrheim, H.: Slicing techniques for verification re-use. Theor. Comput. Sci. 343(3), 509–528 (2005) · Zbl 1079.68061
[27] Weiser, M.: Program slicing. IEEE Transactions on Software Engineering 10(4), 352–357 (1984) · Zbl 0552.68004
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.