Overview

Pre-requisites

fmp2rsmVerifier works with model templates created in RSM using fmp2rsm plug-in. Please refer to fmp2rsm and fmp plug-ins' home pages for more information on how to create feature models and annotate UML model template elements with presence conditions in which features are variables.

Writing user-defined rules

OCL rules to be checked are stored in well-formedness-rules.xml file. To add a user-defined rule, open the file in any xml editor. The structure of the file is as follows:

<well_formedness_rules> <!-- root of the well-formedness-rules list --!>

   <rule> <!-- beginning of a new well-formedness rule --!>

      <errorMessage> <!--
user defined error message, which will appear on problems list --!>

            Dangling association

      </errorMessage>

      <context>Association</context><!-- context metaclass --!>

      <invariant> <!-- OCL invariant definition. Note, that you must put > and < instead of < and > --!>

            self.memberEnd -> size() > 1 and self.memberEnd -> forAll(p.type -> isDefined())

</invariant>

   </rule>

   <rule> ... </rule>

</well_formedness_rules>

Verifying rules

Ones the set of rules is defined, you can verify the model template against it:

Put the well-formedness-rules.xml file into runtime-workspace directory.

Open a feature model with features, which were used to annotate model template elements.

Make sure that the Template Problem List view is opened. It not, open in from Windows/Views/Others/Template Problem List.

Right-click on the root feature and choose fmp2rsm/Verify All Template Instances. The verification process is now started. Whenever an error is found, it a appears on the list of template problems.

Viewing errors

The error row on the list of errors consists of number of incorrect model template instances, error message and example of configuration of feature model leading to incorrect template instance. Whenever new error appear on the list, one can click on error icon to highlight the area of model template including all model elements involved in error.

Performance issues

The verification thread works in background, so there is no need to wait until it is done. You can perform an analysis of the errors as they appear on the template verification problem list. The length of verification process depends linearly on a size of the model. Although it also depends on complexity of the user-defined OCL invariants. Some OCL operations, such as size(), are exponential with regards to new OCL semantics defined for model templates (see Examples & Papers). Therefore, although the verification algorithm is itself sound and complete, there is a need of preset timeout (2 seconds by default) for evaluation of each rule. After this time, the verification procedure of the particular rule on the particular template element is canceled. Then, for complex rules, it's possible that not all errors will be listed. Further work is needed to enable user-defined timeouts and unable-to-prove-on-time message.