Feature Specification and Automatic Conflict Detection

We present a formal feature specification language and a method of automatically detecting feature conflicts ("bad interactions") at the specification stage. Early conflict detection can help prevent costly and time-consuming problem fixes during implementation. Features are specified in linear temporal logic; two features conflict essentially if their specifications are mutually inconsistent under axioms about the underlying system behavior. We show how this inconsistency check may be performed automatically with existing model checking tools. The model checking tools can also be used to provide witness scenarios, both when two features conflict as well as when the features are mutually consistent. Both types of witnesses are useful for refining the specifications. We have implemented a conflict detection tool, FIX (Feature Interaction eXtractor), that uses the model-checker COSPAN for the inconsistency check. We describe our experience in applying this tool to a collection of feature specifications derived from the Bellcore (Telcordia) standards.