Proceedings. 19th International Conference on Automated Software Engineering, 2004. (2004)
Sept. 20, 2004 to Sept. 24, 2004
Colin Blundell , University of Pennsylvania
Kathi Fisler , WPI
Shriram Krishnamurthi , Brown University
Pascal Van Hentenryck , Brown University
Software product-lines view systems as compositions of features. Each component corresponds to an individual feature, and a composition of features yields a product. Feature-oriented verification must be able to analyze individual features and to compose the results into results on products. Since features interact through shared data, verifying individual features entails open system verification concerns. To verify temporal properties, features must be open to both propositional and temporal information from the remainder of the composed product. This paper addresses both forms of openness through a two-phase technique. The first phase analyzes individual features and generates sufficient constraints for property preservation. The second phase discharges the constraints upon composition of features into a product. We present the technique as well as the results of a case study on an email protocol suite.
C. Blundell, S. Krishnamurthi, K. Fisler and P. V. Hentenryck, "Parameterized Interfaces for Open System Verification of Product Lines," Proceedings. 19th International Conference on Automated Software Engineering, 2004.(ASE), Linz, Austria, 2004, pp. 258-267.