Semantics Description Of UML2.0 Sequence Diagrams Using The Temporal Logical Language XYZ/E

In the UML specification, model's syntax is designed with UML class diagrams asmetamodel, while the static semantics is described by OCL and the dynamic semantics isdescribed with English language. This method cannot ensure the completeness,consistency and precise of designs, and it may bring massive effect to the subsequentworks in the software development cycle. Sequence diagram is one of the most importantdynamic diagrams in UML, so the correct, complete and consistent semantics of sequencediagrams is helpful for the rigid analysis and correct verification of complex systemmodels, as well as for the systems development.UML2.0 sequence diagrams are used to describe objects' dynamic interactivebehaviors with the emphasis on expressing the time sequence of messages exchangeswithout rigid time constrains. It is able to describe its semantics with appropriate temporallogical languages. XYZ/E is an executable linear temporal logical language, which canrepresent both dynamic behavior and procedure features. Formally specified by XYZ/E,sequence diagrams can be analyzed under the unified temporal logical framework.Since describing the semantics of sequence diagrams directly is difficult, so we try toseek an intermediate model. The method of control flow analysis is used to construct theintermediate model. An appropriate activity diagram among the six well-defined UML2.0 activity diagrams is chosen and extended to so-called concurrent control flow graph(CCFG) as the intermediate model. A set of OCL-based mappings between a sequencediagram and a CCFG are defined. Then a temporal logical semantics of sequencediagrams is given based on the CCFG using XYZ/E. Finally, the applicability andfeasibility of the approach is shown with a case study.