Abstract
Practical program verification techniques must align with the software development methodologies that produce the programs. Numerous researchers have independently proposed models of program development in which modules encapsulate units of end-user functionality known as features. Such encapsulation reflects user concerns into a program’s modular structure, which in turn promises to simplify program maintenance in the face of requirements evolution. The interplay between feature-oriented modules and verification raises some interesting challenges and opportunities. Such modules ameliorate some difficulties with conventional modular verification, such as property decomposition, while creating others, by contradicting assumptions that underlie most modular program verification techniques. This paper motivates the decomposition of systems by features and provides an overview of the promises and challenges it poses to verification.
This work is partially funded by NSF grants CCR-0305834, CCR-0132659, CCR-0447509 and CCR-0305950.
Chapter PDF
Similar content being viewed by others
Keywords
- Model Check
- Software Product Line
- Parallel Composition
- Automate Software Engineer
- Software Development Methodology
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Jackson, M.: Why software writing is difficult and will remain so. Information Processing Letters 88, 13–25 (2003)
Eliot, T.S.: The love song of J. Alfred Prufrock. In: Prufrock and Other Observations, The Egoist, Ltd., London (1917)
Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17, 507–534 (1995)
Xie, F., Browne, J.C.: Verified systems by composition from verified components. In: Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 277–286. ACM Press, New York (2003)
Szyperski, C.: Component Software: Beyond Object-Oriented Programming. Addison-Wesley, Reading (1998)
Aßmann, U.: Invasive Software Composition. Springer, Heidelberg (2003)
Batory, D.: Feature-oriented programming and the AHEAD tool suite. In: International Conference on Software Engineering (2004)
Batory, D., O’Malley, S.: The design and implementation of hierarchical software systems with reusable components. ACM Transactions on Software Engineering and Methodology 1, 355–398 (1992)
Findler, R.B., Flatt, M.: Modular object-oriented programming with units and mixins. In: ACM SIGPLAN International Conference on Functional Programming, pp. 94–104 (1998)
Harrison, W., Ossher, H.: Subject-oriented programming: a critique of pure objects. In: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications, pp. 411–428 (1993)
Jackson, M., Zave, P.: Distributed feature composition: A virtual architecture for telecommunications services. IEEE Transactions on Software Engineering 24, 831–847 (1998)
Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C.V., Loingtier, J.M., Irwin, J.: Aspect-oriented programming. In: European Conference on Object-Oriented Programming (1997)
Lieberherr, K.J.: Adaptive Object-Oriented Programming. PWS Publishing, Boston (1996)
Mezini, M., Lieberherr, K.: Adaptive plug-and-play components for evolutionary software development. In: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications, pp. 97–116 (1998)
Smaragdakis, Y., Batory, D.: Implementing layered designs and mixin layers. In: European Conference on Object-Oriented Programming, pp. 550–570 (1998)
van Ommering, R.: Building Product Populations with Software Components. PhD thesis, Rijksuniversitat Groningen (2004)
Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley, Reading (2002)
Blundell, C., Fisler, K., Krishnamurthi, S., Hentenryck, P.V.: Parameterized interfaces for open system verification of product lines. In: IEEE International Conference on Automated Software Engineering (2004)
Fisler, K., Krishnamurthi, S.: Modular verification of collaboration-based software designs. In: Symposium on the Foundations of Software Engineering, pp. 152–163. ACM Press, New York (2001)
Li, H.C., Krishnamurthi, S., Fisler, K.: Modular verification of open features through three-valued model checking. Automated Software Engineering 12, 349–382 (2005)
Keck, D.O., Kuehn, P.J.: The feature and service interaction problem in telecommunications systems: A survey. IEEE Transactions on Software Engineering 24, 779–796 (1998)
Valiant, L.G.: A bridging model for parallel computation. Communications of the ACM 33, 103–111 (1990)
Ancona, D., Lagorio, G., Zucca, E.: Jam—designing a Java extension with mixins. ACM Transactions on Programming Languages and Systems 25, 641–712 (2003)
Flatt, M., Krishnamurthi, S., Felleisen, M.: Classes and mixins. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 171–183 (1998)
Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., Zenger, M.: An overview of the Scala programming language. Technical Report IC/2004/64, EPFL Lausanne, Switzerland (2004)
Schärli, N., Ducasse, S., Nierstrasz, O., Black, A.: Traits: Composable units of behavior. In: European Conference on Object-Oriented Programming, pp. 248–274 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Fisler, K., Krishnamurthi, S. (2008). Decomposing Verification Around End-User Features. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)