计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2008年
10期
43-47
,共5页
郭伟%缪力%张大方%闵应骅
郭偉%繆力%張大方%閔應驊
곽위%무력%장대방%민응화
模型检查%Statechart%Statechart山脉算法%迁移提取%Spin
模型檢查%Statechart%Statechart山脈算法%遷移提取%Spin
모형검사%Statechart%Statechart산맥산법%천이제취%Spin
UML已经是软件建模方面的标准语言,UML Statechart描述了系统在其生命周期中的动态行为.随着系统规模的扩大和复杂度的提高,Statechart往往包含设计者所未预料到的隐患,通过模型检查对Statechart进行穷举检验就成为一个重要的课题,首先给出了含层次、并发Statechart的语义;随后提出了对Statechart进行模型检查的一种新方法,并且已经编写软件SC2Spin实现此方法,该方法使用了提出的Statechart山脉算法和迁移提取法,可以将一个Statechart自动转化Spin的输入语言Promela,从而验证Statechart的死锁、活锁等错误和时序逻辑公式.
UML已經是軟件建模方麵的標準語言,UML Statechart描述瞭繫統在其生命週期中的動態行為.隨著繫統規模的擴大和複雜度的提高,Statechart往往包含設計者所未預料到的隱患,通過模型檢查對Statechart進行窮舉檢驗就成為一箇重要的課題,首先給齣瞭含層次、併髮Statechart的語義;隨後提齣瞭對Statechart進行模型檢查的一種新方法,併且已經編寫軟件SC2Spin實現此方法,該方法使用瞭提齣的Statechart山脈算法和遷移提取法,可以將一箇Statechart自動轉化Spin的輸入語言Promela,從而驗證Statechart的死鎖、活鎖等錯誤和時序邏輯公式.
UML이경시연건건모방면적표준어언,UML Statechart묘술료계통재기생명주기중적동태행위.수착계통규모적확대화복잡도적제고,Statechart왕왕포함설계자소미예료도적은환,통과모형검사대Statechart진행궁거검험취성위일개중요적과제,수선급출료함층차、병발Statechart적어의;수후제출료대Statechart진행모형검사적일충신방법,병차이경편사연건SC2Spin실현차방법,해방법사용료제출적Statechart산맥산법화천이제취법,가이장일개Statechart자동전화Spin적수입어언Promela,종이험증Statechart적사쇄、활쇄등착오화시서라집공식.
