A Case Study in Using ACL2 for Feature-Oriented Verification

Feature-oriented software systems are built from components that encapsulate cohesive end-user features. Feature-oriented components are interesting because they cross-cut the system architecture, capturing behavior fragments from several system entities. Features support a plug-and-play style of software construction, in which several systems can be constructed from the same core set of features. This approach requires novel forms of formal verification that support modular reasoning about feature-based components. This paper presents a case study on modeling and verifying a feature-oriented email system in ACL2. The main goal of the study is to identify classes of theorems that should be proven about individual features so that properties about compositions of features can be derived from the theorems on the individual features. A secondary goal is to evaluate ACL2 as a modeling and verification framework for feature-oriented systems. We present our feature model and insights into verification, then discuss the strengths and weaknesses of ACL2 in this problem domain.