Ferruccio Damiani
Olaf Owe
ABSTRACT
Delta-oriented programming is a modular, yet flexible technique to implement software product lines. To efficiently verify the specifications of all possible product variants of a product line, it is usually infeasible to generate all product variants and to verify them individually. To counter this problem, we propose a transformational proof system in which the specifications in a delta module describe changes to previous specifications. Our approach allows each delta module to be verified in isolation, based on symbolic assumptions for calls to methods which may be in other delta modules. When product variants are generated from delta modules, these assumptions are instantiated by the actual guarantees of the methods in the considered product variant and used to derive the specifications of this product variant.
- S. Apel, C. Kästner, A. Grösslinger, and C. Lengauer. Type safety for feature-oriented product lines. Automated Software Engineering, 17(3): 251--300, 2010. Google Scholar
Digital Library
- K. R. Apt. Ten years of Hoare's logic: A survey --- Part I. ACM TOPLAS, 3(4): 431--483, Oct. 1981. Google ScholarDigital Library
- K. R. Apt, F. S. de Boer, and E.-R. Olderog. Verification of Sequential and Concurrent Systems. Springer, 2009. Google ScholarDigital Library
- P. Asirelli, M. H. ter Beek, S. Gnesi, and A. Fantechi. Deontic logics for modeling behavioural variability. In VaMoS, pp. 71--76, January 2009.Google Scholar
- D. Batory. Feature Models, Grammars, and Propositional Formulas. In SPLC, LNCS 3714, pp. 7--20. Springer, 2005. Google ScholarDigital Library
- D. S. Batory and E. Börger. Modularizing theorems for software product lines: The Jbook case study. J. UCS, 14(12): 2059--2082, 2008.Google Scholar
- B. Beckert, R. Hähnle, and P. H. Schmitt, editors. Verification of Object-Oriented Software: The KeY Approach, LNCS 4334. Springer, 2007. Google ScholarDigital Library
- L. Bettini, F. Damiani, D. Meglio, I. Schaefer, and F. Strocco. DeltaJ website (New Version), September 2011. http://deltaj.sourceforge.net/.Google Scholar
- D. Bruns, V. Klebanov, and I. Schaefer. Verification of software product lines with delta-oriented slicing. In FoVeOOS 2010, LNCS 6528. Springer, 2011. Google ScholarDigital Library
- 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. IEEE, 2010. Google ScholarDigital Library
- F. S. de Boer. A WP-calculus for OO. In FOSSACS, LNCS 1578, pp. 135--149. Springer, 1999. Google ScholarDigital Library
- B. Delaware, W. Cook, and D. Batory. A Machine-Checked Model of Safe Composition. In FOAL, pp. 31--35. ACM, 2009. Google ScholarDigital Library
- B. Delaware, W. Cook, and D. Batory. Theorem Proving for Product Lines. In OOPSLA'11, 2011.Google Scholar
- J. Dovland, E. B. Johnsen, O. Owe, and M. Steffen. Lazy behavioral subtyping. Journal of Logic and Algebraic Programming, 79(7): 578--607, 2010.Google ScholarCross Ref
- R. Hähnle and I. Schafer. A Liskov Principle for Delta-oriented Programming. In FoVeOOS 2011, LNCS 7421. Springer, 2012.Google Scholar
- C. A. R. Hoare. An Axiomatic Basis of Computer Programming. Comm. ACM, 12: 576--580, 1969. Google ScholarDigital Library
- S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4): 319--340, 1976.Google ScholarDigital Library
- I. Schaefer, L. Bettini, V. Bono, F. Damiani, and N. Tanzarella. Delta-oriented Programming of Software Product Lines. In SPLC, LNCS 6287, pp. 77--91. Springer, 2010. Google ScholarDigital Library
- I. Schaefer, L. Bettini, and F. Damiani. Compositional Type-Checking for Delta-Oriented Programming. In AOSD. ACM, 2011. Google ScholarDigital Library
- I. Schaefer and R. Hähnle. Formal methods in software product line engineering. IEEE Computer, 44(2): 82--85, 2011. Google ScholarDigital Library
- T. Thüm, S. Apel, C. Kästner, M. Kuhlemann, I. Schaefer, and G. Saake. Analysis Strategies for Software Product Lines. Tech. Rep. FIN-004-2012, School of Comp. Science, Univ. of Magdeburg, Germany, Apr. 2012.Google Scholar
- T. Thüm, I. Schaefer, M. Kuhlemann, and S. Apel. Proof composition for deductive verification of software product lines. In VAST, pp. 270--277. IEEE, 2011. Google ScholarDigital Library
Index Terms
- A transformational proof system for delta-oriented programming
Recommendations
Pure delta-oriented programming
FOSD '10: Proceedings of the 2nd International Workshop on Feature-Oriented Software DevelopmentDelta-oriented programming (DOP) is a modular approach for implementing software product lines. Delta modules generalize feature modules by allowing removal of functionality. However, DOP requires to select one particular product as core product from ...
Compositional type-checking for delta-oriented programming
AOSD '11: Proceedings of the tenth international conference on Aspect-oriented software developmentDelta-oriented programming is a compositional approach to flexibly implementing software product lines. A product line is represented by a code base and a product line declaration. The code base consists of a set of delta modules specifying ...
Dynamic delta-oriented programming
SPLC '11: Proceedings of the 15th International Software Product Line Conference, Volume 2Modern software systems should be designed to dynamically adapt to changing user requirements or resource constraints. Delta-oriented programming (DOP) is a compositional approach to flexibly implement software product lines. In DOP, a product line is ...
Comments