%0 Journal Article
%T uml状态机的形式语义
%A 蒋慧？
%A 林东？
%A 谢希仁？
%J 软件学报
%P 2244-2250
%D 2002
%X 许多大型系统在进行分析和设计时,均采用uml作为需求描述语言,尤其是一些对安全性要求较高的系统,更是广泛采用uml的动态行为描述机制--状态机来描述协议及控制机制.但是,由于uml没有形式化的动态语义,不利于对其所描述的需求进行形式化验证和证明.为了解决这一问题,采用以下方法为uml状态机构建形式语义.把uml状态机中的状态映射到一种项代数上,用归纳的状态项表示状态机的状态.然后,把状态项映射到一种加标记的变迁系统lts上,lts-状态是状态机的状态项,lts-变迁是uml状态机的微步.最后,用plotk
%K uml状态机
%K 形式语义
%K 结构化操作语义(structural
%K operational
%K semantics
%K 简称sos)
%K 状态图
%K 加标记的变迁系统
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20021205&flag=1