Modern technical systems typically consist of multiple components and must provide many functions that are realized by the complex interaction of these components. Moreover, very often not only a single product, but a whole product line with different compositions of components and functions must be developed. To cope with this complexity, it is important that engineers have intuitive, but precise means for specifying the requirements for these systems and have tools for automatically finding inconsistencies within the requirements, because these could lead to costly iterations in the later development.
We propose a scenario-based approach for the intuitive, but precise specification of product lines and present a novel technique for efficiently consistency checking the specification of all the variants in a product line. The approach is based on Modal Sequence Diagrams (MSDs) and Feature Diagrams for specifying a product line. The consistency can be checked by using a novel model-checking technique for feature transition systems (more information can be found here).
As shown in the figure below, our approach supports the requirements engineer in the scenario-based specification of a product line. For this purpose, we have created a lightweight extension of UML, so that scenario-based product line specifications can be created with standard UML edtitors. A scenario-based product line specification can be transformed into an SMV model (or, more precisely, a “feature enriched” fSMV model) where an extended version of the NuSMV model checker can now check whether the specification of all product variants is consistent or not. If not, the tool will give counter-examples for product variants where the specification is inconsistent. These counter-examples are sequences of events in the system that lead to an inevitable violation of the specification. With this information, the requirements engineer can correct or refine the specification.
- Overview of the scenario-based product lines specification and consistency checking approach
The transformation is described by a Triple Graph Grammar (TGG) that can be executed by the TGG-Interpreter.
- Instructions for installing the tool can be found here.
- Instructions for using the tool can be found here.
- An explanation of some example product line specifications and resulting fSMV models are coming soon.
This tool was created in joint work with Maxime Cordy, Patrick Heymans, and Amir Sharifloo.