%0 Journal Article %T The Formal Semantics of UML State Machine
UML状态机的形式语义 %A JIANG Hui %A LIN Dong %A XIE Xi-ren %A
蒋慧 %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
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