fmp2rsmVerifier is a research prototype of a model template verifier plug-in for Eclipse/RSM. It verifiers if all instances of the model template (created in Rational Software Modeler using fmp2rsm plug-in) are correct with respect to the set of well-formedness rules. These rules are user-defined OCL invariants written with regards to target notation, in our case UML metamodel.
Current Version: 0.1.1 - research prototype
Project status: Completed
Team Members
News
Publications
2006
Czarnecki, K., and K. Pietroszek,
"Verifying feature-based model templates against well-formedness OCL constraints",
5th international conference on Generative programming and component engineering - GPCE '06, Portland, Oregon, USA, ACM Press, pp. 211, 2006.
[pdf]
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.