%0 Journal Article
%T Formal Semantics of Universal Modal Sequence Diagram<br>模态顺序图uMSD 的形式语义
%A LI Wen-Rui
%A WANG Zhi-Jian
%A ZHANG Peng-Cheng
%A <br>李雯睿
%A 王志坚
%A 张鹏程
%J 软件学报
%D 2011
%I 
%X The UML 2.0 Sequence Diagram has been extensively applied in industry. However, the vague semantics of UML 2.0 Sequence Diagram prevent it from being applied effectively. Modal Sequence Diagram is the modal extension of UML 2.0 Sequence Diagram, which distinguishes mandatory scenarios (described by universal MSD, denoted as uMSD) from possible scenarios (described by existential MSD, denoted as eMSD). uMSD is more expressive than eMSD and can represent the temporal properties of concurrent systems. Therefore, the main work of the paper is on uMSD. In order to make uMSD extensively used for formal analysis, verification, and monitoring, the formal semantics of uMSD, based on the Weak Alternating Büchi automaton, are represented, and the transformation algorithms of various operators are given in detail. Next, the expressiveness of uMSD is measured by the well known property specification patterns. Finally, an example is studied, and its future applications are discussed.
%K 模态顺序图
%K 弱交换Büchi
%K 自动机
%K 性质规约模式
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=20995FE72A2BCA03A6F53D6C049F7F54&yid=9377ED8094509821&vid=BC12EA701C895178&iid=E158A972A605785F&sid=00520952CD4BF212&eid=DEE640F0CDC9D495&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=14