marte顺序图到tts4sd的转换

marte对um工的顺序图进行了扩充，使其适用于实时系统的建模阶段，但它不能直接用于正确性验证阶段。对象管理组织提出用模型转换的方法将依照marte构造的顺序图(记为a)转换成具有完备的验证方法和工具的形式化模型(记为b)。用b表示a的语义可以保证i3能够完整且准确地模拟a的行为。提出了形式化模型=tts4sd，用来描述marte顺序图的形式语义，并在此基础上展开了验证。首先给出顺序图的形式定义，把时间变迁系统(tts)扩充成tts4sd;然后用tts4sd描述顺序图的形式语义，并给出从顺序图到tts4sd的转换算法;最后对tts4sd展开分析。通过一个实例说明了从顺序图到tts4sd的转化过程以及基于tts4sd的验证方法。