%0 Journal Article %T The Formal Semantics of UML Sequence Diagram Based on Process Algebra
基于进程代数的UML序列图的形式语义 %A LI Qing-Shan ZHU Hua CHEN Ping %A
李青山 %A 褚华 %A 陈平 %J 计算机科学 %D 2004 %I %X UML Sequence diagram models interactions between instances, but UML has no strictly defined formal dynamic semantics. So it is difficult to do formal verification and proof on the models. In this paper,based on the mapping of the actions of sequence diagram to the process expressions of process algebra,a formal semantics of UML sequence diagram is built. First .mapping rules are given between sequence diagram and process algebra,and next a set of Plotkin-stylc structural operational semantics is used to define inductive rules for composition operator of UML sequence diagram process algebra. Finally, we introduce ordering constraints conditions for compositional operator and prove it's property of termination. %K UML sequence diagram %K Formal semantics %K Process algebra %K Composition operator %K Structural operational semantics
面向对象 %K 建模语言 %K UML %K 进程代数 %K 序列图 %K 形式语义 %U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=6A270C7E55E2B52F&yid=D0E58B75BFD8E51C&vid=4AD960B5AD2D111A&iid=E158A972A605785F&sid=DABEF202280E7EF1&eid=A58CF3BAE79427D0&journal_id=1002-137X&journal_name=计算机科学&referenced_num=3&reference_num=10