| Popis: |
In this paper, we propose a new approach to formally analyze UML CombinedFragments. The latter are mapped into Colored Petri Nets, or CPN. The derived specification is value-oriented, composed of identified objects and events, thus allowing for a more precise analysis of the model behavior. To verify that the CPN model preserves the system properties, we use OCL invariants. This use induces the need for specifying the association ends on the behavioral models. The analysis results are in the form of CPNTools reports. They, consequently, are not necessarily comprehensible to UML designers. Automatic analysis of the CPNTools results is, therefore, provided. It is followed by an interpretation of these results and their feedback to the user, expressed in UML language. |
