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 real time system, however, it is not easy to verify due to its informal semantics. An extended time Petri net (TPN) with \emph{weak} semantics–TLOPNforSD–is defined and proved to be decidable as far as reach ability, boundedness and cover ability 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 \emph{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.