The Profile for the Modeling and Analysis of Real-Time Embedded Systems (MARTE) provides an extended sequence diagram with time properties (SDT). This kind of diagram is frequently used in the preliminary developing phase of the embedded real time systems (ERTS), however, it is not easy to verify the system it has described because few tools can check it directly. This is mainly due to its semi-formal style and its abstract mode in describing the behaviors of the corresponding system. The formal definition of the SDT is firstly introduced, and an extended model named timed transition system for SDT (TTS4SDT) is advanced for describing its formal semantics. By model transformation techniques, the SDT is transformed to the intermediate model--TTS4SDT, and the transforming methods are divided into two categories: when the SDT doesn't equip with nesting structures and when it does. Two examples (one is without nesting structure and another is with) are offered to demonstrate the transforming process. Then based on the TTS4SDT, the sequence diagram is analyzed in a rigid way to eliminate the mistakes arising from the designing stage.