计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2013年
1期
175-178
,共4页
实时系统%顺序图%CCSL%形式化方法%模型转换
實時繫統%順序圖%CCSL%形式化方法%模型轉換
실시계통%순서도%CCSL%형식화방법%모형전환
MARTE对UML的顺序图进行了扩充,使其适用于实时系统的建模阶段,但它不能直接用于正确性验证阶段.对象管理组织提出用模型转换的方法将依照MARTE构造的顺序图(记为A)转换成具有完备的验证方法和工具的形式化模型(记为B).用B表示A的语义可以保证B能够完整且准确地模拟A的行为.提出了形式化模型——TTS4SD,用来描述MARTE顺序图的形式语义,并在此基础上展开了验证.首先给出顺序图的形式定义,把时间变迁系统(TTS)扩充成TTS4SD;然后用TTS4SD描述顺序图的形式语义,并给出从顺序图到TTS4SD的转换算法；最后对TTS4SD展开分析.通过一个实例说明了从顺序图到TTS4SD的转化过程以及基于TTS4SD的验证方法.
MARTE對UML的順序圖進行瞭擴充,使其適用于實時繫統的建模階段,但它不能直接用于正確性驗證階段.對象管理組織提齣用模型轉換的方法將依照MARTE構造的順序圖(記為A)轉換成具有完備的驗證方法和工具的形式化模型(記為B).用B錶示A的語義可以保證B能夠完整且準確地模擬A的行為.提齣瞭形式化模型——TTS4SD,用來描述MARTE順序圖的形式語義,併在此基礎上展開瞭驗證.首先給齣順序圖的形式定義,把時間變遷繫統(TTS)擴充成TTS4SD;然後用TTS4SD描述順序圖的形式語義,併給齣從順序圖到TTS4SD的轉換算法；最後對TTS4SD展開分析.通過一箇實例說明瞭從順序圖到TTS4SD的轉化過程以及基于TTS4SD的驗證方法.
MARTE대UML적순서도진행료확충,사기괄용우실시계통적건모계단,단타불능직접용우정학성험증계단.대상관리조직제출용모형전환적방법장의조MARTE구조적순서도(기위A)전환성구유완비적험증방법화공구적형식화모형(기위B).용B표시A적어의가이보증B능구완정차준학지모의A적행위.제출료형식화모형——TTS4SD,용래묘술MARTE순서도적형식어의,병재차기출상전개료험증.수선급출순서도적형식정의,파시간변천계통(TTS)확충성TTS4SD;연후용TTS4SD묘술순서도적형식어의,병급출종순서도도TTS4SD적전환산법；최후대TTS4SD전개분석.통과일개실례설명료종순서도도TTS4SD적전화과정이급기우TTS4SD적험증방법.
