Although model checking is extensively used for verification of single software systems, currently there is insufficient support for model checking in product lines. The presence of commonalities within the different products in the product line requires that the properties and the corresponding specifications for these properties be verified for every product in the product line. Specification and management of properties for every product in a product line can incur high overhead and make the task of model checking very difficult. It is hence essential to exploit the presence of commonalities to our advantage by providing reusability in model checking of product lines. Since different products in the product line need to be checked for same or similar properties, reuse of properties specified for one product for other products within a product line will significantly reduce the overall property specification and verification time.

FormulaEditor is a property specification and management tool for enhancing the reusability of model checking of software product lines. The core of the technique is a product line-oriented user interface to guide users in generating, selecting, managing, and reusing useful product line properties, and patterns of properties for model checking. The previous version of the FormulaEditor tool supports Cadence SMV models, but not the typical CMU-SMV models. This work extends the FormulaEditor tool to allow verification of models written in CMU-SMV. The advantage of providing support to another model checker is twofold: first, it enhances the tool’s capability to check design specifications written in different models; and second, it allows users to specify the same design in different modeling languages to detect problems.