软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2011年
4期
659-675
,共17页
模态顺序图%弱交换Büchi自动机%性质规约模式
模態順序圖%弱交換Büchi自動機%性質規約模式
모태순서도%약교환Büchi자동궤%성질규약모식
UML 2.0顺序图已广泛应用于业界,但其语义模糊,以至于不能有效地加以使用.模态顺序图(modal sequence diagram,简称MSD)是对UML 2.0顺序图的模态扩展,区分了强制场景(用universal MSD表示,简称uMSD)和可能场景(用existential MSD表示,简称eMSD).其中,uMSD具有较强的表达能力,能够用于表示并发系统的时态性质,故主要工作围绕uMSD展开.为了使uMSD用于形式化分析、验证和监控,给出基于自动机的uMSD语义解释,并给出各种操作符的算法,用性质规约模式度量uMSD的表达能力.最后进行了实例研究,并讨论了其应用前景.
UML 2.0順序圖已廣汎應用于業界,但其語義模糊,以至于不能有效地加以使用.模態順序圖(modal sequence diagram,簡稱MSD)是對UML 2.0順序圖的模態擴展,區分瞭彊製場景(用universal MSD錶示,簡稱uMSD)和可能場景(用existential MSD錶示,簡稱eMSD).其中,uMSD具有較彊的錶達能力,能夠用于錶示併髮繫統的時態性質,故主要工作圍繞uMSD展開.為瞭使uMSD用于形式化分析、驗證和鑑控,給齣基于自動機的uMSD語義解釋,併給齣各種操作符的算法,用性質規約模式度量uMSD的錶達能力.最後進行瞭實例研究,併討論瞭其應用前景.
UML 2.0순서도이엄범응용우업계,단기어의모호,이지우불능유효지가이사용.모태순서도(modal sequence diagram,간칭MSD)시대UML 2.0순서도적모태확전,구분료강제장경(용universal MSD표시,간칭uMSD)화가능장경(용existential MSD표시,간칭eMSD).기중,uMSD구유교강적표체능력,능구용우표시병발계통적시태성질,고주요공작위요uMSD전개.위료사uMSD용우형식화분석、험증화감공,급출기우자동궤적uMSD어의해석,병급출각충조작부적산법,용성질규약모식도량uMSD적표체능력.최후진행료실례연구,병토론료기응용전경.
