%0 Journal Article
%T The Formal Semantics of UML State Machine<br>UML状态机的形式语义
%A JIANG Hui
%A LIN Dong
%A XIE Xi-ren
%A <br>蒋慧
%A 林东
%A 谢希仁
%J 软件学报
%D 2002
%I 
%X 许多大型系统在进行分析和设计时,均采用UML作为需求描述语言,尤其是一些对安全性要求较高的系统,更是广泛采用UML的动态行为描述机制--状态机来描述协议及控制机制.但是,由于UML没有形式化的动态语义,不利于对其所描述的需求进行形式化验证和证明.为了解决这一问题,采用以下方法为UML状态机构建形式语义.把UML状态机中的状态映射到一种项代数上,用归纳的状态项表示状态机的状态.然后,把状态项映射到一种加标记的变迁系统LTS上,LTS-状态是状态机的状态项,LTS-变迁是UML状态机的微步.最后,用Plotk
%K UML state machine
%K formal semantics
%K SOS(structural operational semantics)
%K statechart
%K labeled transition system<br>UML状态机
%K 形式语义
%K 结构化操作语义(structural
%K operational
%K semantics
%K 简称SOS)
%K 状态图
%K 加标记的变迁系统
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=722D71A7D27BA977&yid=C3ACC247184A22C1&vid=FC0714F8D2EB605D&iid=59906B3B2830C2C5&sid=2C502C9A2A834A49&eid=28C569C68A441089&journal_id=1000-9825&journal_name=软件学报&referenced_num=16&reference_num=15