计算机工程与设计
計算機工程與設計
계산궤공정여설계
COMPUTER ENGINEERING AND DESIGN
2012年
9期
3460-3464
,共5页
侯敏%宋文鹏%王泊涵%王新冶
侯敏%宋文鵬%王泊涵%王新冶
후민%송문붕%왕박함%왕신야
UML状态机%模型检查%形式化验证%符号模型检查器
UML狀態機%模型檢查%形式化驗證%符號模型檢查器
UML상태궤%모형검사%형식화험증%부호모형검사기
系统建模是系统开发经常用到的分析设计方法,如何保证模型的正确性一直是人们关注的话题.为了验证系统设计的模型正确性,进而提高整个系统的质量,提出了一种通过模型检查技术对UML状态机模型进行动态语义验证的方法.对状态机模型进行形式化描述,根据定义的映射规则将图形信息映射成模型检查器可以读取的语言,分析待验证的性质内容,通过使用模型检查器得到验证结果.
繫統建模是繫統開髮經常用到的分析設計方法,如何保證模型的正確性一直是人們關註的話題.為瞭驗證繫統設計的模型正確性,進而提高整箇繫統的質量,提齣瞭一種通過模型檢查技術對UML狀態機模型進行動態語義驗證的方法.對狀態機模型進行形式化描述,根據定義的映射規則將圖形信息映射成模型檢查器可以讀取的語言,分析待驗證的性質內容,通過使用模型檢查器得到驗證結果.
계통건모시계통개발경상용도적분석설계방법,여하보증모형적정학성일직시인문관주적화제.위료험증계통설계적모형정학성,진이제고정개계통적질량,제출료일충통과모형검사기술대UML상태궤모형진행동태어의험증적방법.대상태궤모형진행형식화묘술,근거정의적영사규칙장도형신식영사성모형검사기가이독취적어언,분석대험증적성질내용,통과사용모형검사기득도험증결과.
