| UML状态机的形式语义 |
| |
| 引用本文： | 蒋慧,林东,谢希仁.UML状态机的形式语义[J].软件学报,2002,13(12):2244-2250. |
| |
| 作者姓名： | 蒋慧 林东 谢希仁 |
| |
| 作者单位： | 1. 解放军理工大学计算机系,江苏,南京,210007
2. 国防大学战略教研室,北京,100091 |
| |
| 基金项目： | 国家自然科学基金资助项目(69931040) |
| |
| 摘 要： | 许多大型系统在进行分析和设计时,均采用UML作为需求描述语言,尤其是一些对安全性要求较高的系统,更是广泛采用UML的动态行为描述机制--状态机来描述协议及控制机制.但是,由于UML没有形式化的动态语义,不利于对其所描述的需求进行形式化验证和证明.为了解决这一问题,采用以下方法为UML状态机构建形式语义.把UML状态机中的状态映射到一种项代数上,用归纳的状态项表示状态机的状态.然后,把状态项映射到一种加标记的变迁系统LTS上,LTS-状态是状态机的状态项,LTS-变迁是UML状态机的微步.最后,用Plotk
|
| 关 键 词： | UML状态机 形式语义 结构化操作语义(structural operational semantics 简称SOS) 状态图 加标记的变迁系统 |
| 文章编号： | 1000-9825/2002/13(12)2244-07 |
| 收稿时间： | 2001/4/17 0:00:00 |
| 修稿时间： | 2001年4月17日 |
The Formal Semantics of UML State Machine |
| |
| JIANG Hui,LIN Dong and XIE Xi-ren.The Formal Semantics of UML State Machine[J].Journal of Software,2002,13(12):2244-2250. |
| |
| Authors: | JIANG Hui LIN Dong and XIE Xi-ren |
| |
| Abstract: | |
| |
| Keywords: | UML state machine formal semantics SOS(structural operational semantics) statechart labeled transition system |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
