Kathi Fisler (Worcester Polytechnic Institute), Parameterized Interfaces for Open System Verification of Product Lines (joint work with Colin Blundell, Shriram Krishnamurthi, and Pascal Van Hentenryck)

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, verification must treat them as open systems. We present a two-phase verification technique for product lines built from features. The first phase generates sufficient constraints on individual features to preserve their desired temporal logic properties. The second phase discharges these constraints upon composition of features into a product. The talk describes our technique and, more generally, the sorts of constraints that appear useful for verification in this context.

• CV06
• Homepages:
  • Newton Institute
  • MPI Informatik
• Organizers:
  • Prof. Moshe Vardi
  • Prof. Andreas Podelski
• Invited Participants
• Application Form
• Search