2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) (2004)
Sept. 20, 2004 to Sept. 24, 2004
Colin Blundell , University of Pennsylvania
Shriram Krishnamurthi , Brown University
Kathi Fisler , WPI
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.
Colin Blundell, Shriram Krishnamurthi, Kathi Fisler, Pascal Van Hentenryck, "Parameterized Interfaces for Open System Verification of Product Lines", 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), vol. 00, no. , pp. 258-267, 2004, doi:10.1109/ASE.2004.10004