%0 Journal Article
%T marte顺序图到tts4sd的转换
%A 朱梅霞
%A 武继刚？
%J 计算机科学
%D 2013
%X marte对um工的顺序图进行了扩充，使其适用于实时系统的建模阶段，但它不能直接用于正确性验证阶段。对象管理组织提出用模型转换的方法将依照marte构造的顺序图(记为a)转换成具有完备的验证方法和工具的形式化模型(记为b)。用b表示a的语义可以保证i3能够完整且准确地模拟a的行为。提出了形式化模型=tts4sd，用来描述marte顺序图的形式语义，并在此基础上展开了验证。首先给出顺序图的形式定义，把时间变迁系统(tts)扩充成tts4sd;然后用tts4sd描述顺序图的形式语义，并给出从顺序图到tts4sd的转换算法;最后对tts4sd展开分析。通过一个实例说明了从顺序图到tts4sd的转化过程以及基于tts4sd的验证方法。
%K 实时系统
%K 顺序图
%K ccsl
%K 形式化方法
%K 模型转换
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=130140&flag=1