苏州市职业大学学报
囌州市職業大學學報
소주시직업대학학보
JOURNAL OF SUZHOU VOCATIONAL UNIVERSITY
2009年
1期
60-65
,共6页
陆公正%吴澜波%于复生%张广泉
陸公正%吳瀾波%于複生%張廣泉
륙공정%오란파%우복생%장엄천
UML Statechart图%数据流语义%时序逻辑%验证%模型检测
UML Statechart圖%數據流語義%時序邏輯%驗證%模型檢測
UML Statechart도%수거류어의%시서라집%험증%모형검측
由于UML Statechart图缺乏精确的数据流语义,因而难以对UML Statechart图建模的工作流的数据流进行正确性验证.首先,UML Statechart图是基于状态转换的,为此选择标记转换系统(LTS)作为语义域,并用结构化操作语义(SOS)分两步定义了UML Statechart图的数据流语义.然后,采用时序逻辑公式表示数据流所需满足的性质,同时给出了将UML Statechart图模型转化为可达状态迁移图的算法,最后通过模型检测算法验证数据流的正确性.
由于UML Statechart圖缺乏精確的數據流語義,因而難以對UML Statechart圖建模的工作流的數據流進行正確性驗證.首先,UML Statechart圖是基于狀態轉換的,為此選擇標記轉換繫統(LTS)作為語義域,併用結構化操作語義(SOS)分兩步定義瞭UML Statechart圖的數據流語義.然後,採用時序邏輯公式錶示數據流所需滿足的性質,同時給齣瞭將UML Statechart圖模型轉化為可達狀態遷移圖的算法,最後通過模型檢測算法驗證數據流的正確性.
유우UML Statechart도결핍정학적수거류어의,인이난이대UML Statechart도건모적공작류적수거류진행정학성험증.수선,UML Statechart도시기우상태전환적,위차선택표기전환계통(LTS)작위어의역,병용결구화조작어의(SOS)분량보정의료UML Statechart도적수거류어의.연후,채용시서라집공식표시수거류소수만족적성질,동시급출료장UML Statechart도모형전화위가체상태천이도적산법,최후통과모형검측산법험증수거류적정학성.
