小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2013年
1期
100-106
,共7页
朱梅霞%王捍贫%刘西奎%韩晓琼
硃梅霞%王捍貧%劉西奎%韓曉瓊
주매하%왕한빈%류서규%한효경
实时系统%形式化方法%MARTE%时间变迁系统%验证
實時繫統%形式化方法%MARTE%時間變遷繫統%驗證
실시계통%형식화방법%MARTE%시간변천계통%험증
作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行验证和精化,以完成A的验证和精化工作.此思想面临的难题是如何保证B能够完整且准确地模拟A的行为.提出了形式化模型-TrS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析.首先给出顺序图的形式定义,把时阃变迁系统(TrS)扩充成TrS4SD,用TrS4SD描述顺序图的形式语义,最后对TrS4SD展开分析.这在一定程度上提高了设计阶段模型的正确性.通过一个实例说明从顺序图到TrS4SD的转化过程以及基于TTS4SD的验证方法.
作為一項新規範,MARTE有許多方麵亟待完善.如何對依照MARTE設計的模型開展驗證是待解決問題之一.對象管理組織提齣用模型轉換的方法將依照MARTE設計的模型(記為A)轉換成另一種具有完備的驗證方法和工具的形式化模型(記為B),然後對B進行驗證和精化,以完成A的驗證和精化工作.此思想麵臨的難題是如何保證B能夠完整且準確地模擬A的行為.提齣瞭形式化模型-TrS4SD,用來描述MARTE規範定義的帶時間約束的順序圖的形式語義併在此基礎上展開分析.首先給齣順序圖的形式定義,把時閫變遷繫統(TrS)擴充成TrS4SD,用TrS4SD描述順序圖的形式語義,最後對TrS4SD展開分析.這在一定程度上提高瞭設計階段模型的正確性.通過一箇實例說明從順序圖到TrS4SD的轉化過程以及基于TTS4SD的驗證方法.
작위일항신규범,MARTE유허다방면극대완선.여하대의조MARTE설계적모형개전험증시대해결문제지일.대상관리조직제출용모형전환적방법장의조MARTE설계적모형(기위A)전환성령일충구유완비적험증방법화공구적형식화모형(기위B),연후대B진행험증화정화,이완성A적험증화정화공작.차사상면림적난제시여하보증B능구완정차준학지모의A적행위.제출료형식화모형-TrS4SD,용래묘술MARTE규범정의적대시간약속적순서도적형식어의병재차기출상전개분석.수선급출순서도적형식정의,파시곤변천계통(TrS)확충성TrS4SD,용TrS4SD묘술순서도적형식어의,최후대TrS4SD전개분석.저재일정정도상제고료설계계단모형적정학성.통과일개실례설명종순서도도TrS4SD적전화과정이급기우TTS4SD적험증방법.
