Decomposing Verification Around End-User Features

摘要

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.