郑州大学学报（理学版）
鄭州大學學報（理學版）
정주대학학보（이학판）
JOURNAL OF ZHENGZHOU UNIVERSITY(NATURAL SCIENCE EDITION)
2013年
1期
50-55
,共6页
统一建模语言%模型验证%模型转换%Uppaal%时间自动机%元模型
統一建模語言%模型驗證%模型轉換%Uppaal%時間自動機%元模型
통일건모어언%모형험증%모형전환%Uppaal%시간자동궤%원모형
针对无法对UML模型进行形式化验证的问题,提出在元模型层将UML模型转换为时间自动机模型并进行验证的方法.形式化UML状态机的结构,抽象出UML和时间自动机的元模型,利用模型转换语言ATL对UML元模型和时间自动机元模型构造映射规则,实现UML模型到时间自动机模型的转换,在模型验证工具Uppaal中对转换结果进行形式化验证.最后进行实例研究,结果表明了此方法的有效性和先进性.
針對無法對UML模型進行形式化驗證的問題,提齣在元模型層將UML模型轉換為時間自動機模型併進行驗證的方法.形式化UML狀態機的結構,抽象齣UML和時間自動機的元模型,利用模型轉換語言ATL對UML元模型和時間自動機元模型構造映射規則,實現UML模型到時間自動機模型的轉換,在模型驗證工具Uppaal中對轉換結果進行形式化驗證.最後進行實例研究,結果錶明瞭此方法的有效性和先進性.
침대무법대UML모형진행형식화험증적문제,제출재원모형층장UML모형전환위시간자동궤모형병진행험증적방법.형식화UML상태궤적결구,추상출UML화시간자동궤적원모형,이용모형전환어언ATL대UML원모형화시간자동궤원모형구조영사규칙,실현UML모형도시간자동궤모형적전환,재모형험증공구Uppaal중대전환결과진행형식화험증.최후진행실례연구,결과표명료차방법적유효성화선진성.
