The Analysis of Sequence Diagram with Time Properties in Qualitative and Quantitative Aspects by Model Transformation

The Sequence Diagram (SD) with time properties is frequently used in the preliminary developing phase of embedded reala time system, however, it is not easy to verify due to its informal semantics. An extended time Petri net (TPN) with weak semantics-TLOPNforSD-is defined and proved to be decidable as far as reachability, boundedness and coverability are concerned. A method for progressively refining the SD is also offered in the transformation phase. The SD with time properties are made to be more reliable in two aspects: (1) an enabled transitions generating algorithm based on weak semantics is designed. Based on this algorithm, the verification of SD with time properties in qualitative aspect can be realized by dint of ROMEO; (2) using the state-class diagram obtained in qualitative analysis phase, a scheduling strategy satisfying all the time constraints specified in the SD is worked out. The strategy is used to get compelling time intervals which are more accurate than the static intervals predefined on the SD for every event.