资源描述：
《UML状态机的形式语意》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、1000-9825/2002/13(12)2244-07©2002JournalofSoftware软件学报Vol.13,No.12UML状态机的形式语义Ã121蒋慧,林东,谢希仁1(解放军理工大学计算机系,江苏南京210007);2(国防大学战略教研室,北京100091)E-mail:osman@263.net;donglin_cn@sina.com;xiexr@public1.ptt.js.cn摘要:许多大型系统在进行分析和设计时,均采用UML作为需求描述语言,尤其是一些对安全性要求较高的系统,更是广泛采用UML的
2、动态行为描述机制——状态机来描述协议及控制机制.但是,由于UML没有形式化的动态语义,不利于对其所描述的需求进行形式化验证和证明.为了解决这一问题,采用以下方法为UML状态机构建形式语义.把UML状态机中的状态映射到一种项代数上,用归纳的状态项表示状态机的状态.然后,把状态项映射到一种加标记的变迁系统LTS上,LTS-状态是状态机的状态项,LTS-变迁是UML状态机的微步.最后,用Plotkin风格的结构操作语义SOS(structuraloperationalsemantics)规则归纳地给出满足组合性的UML状态机
3、语义.此方法既是对一些经典Statechart形式化方法的综合,又针对UML状态机的特点作了创新,使状态项能够动态地描述任意时刻UML状态机的配置树,简化LTS的标记,同时,结构化的语义规则更为形式化验证奠定了基础.关键词:UML状态机;形式语义;结构化操作语义(structuraloperationalsemantics,简称SOS);状态图;加标记的变迁系统中图法分类号:TP311文献标识码:A[1]随着OMG组织采纳UML作为面向对象分析和设计建模语言的标准,UML被广泛使用和推广.许多大型[2]系统均采用UML
4、作为需求描述语言进行分析和设计.但是,尽管UML的静态语义由元模型(meta-model)给出,但其动态语义却十分模糊,不利于对其所描述的需求进行形式化的验证和确认,这一点已经成为阻挠在安全性[3~8]要求高的系统开发中使用UML的主要原因.为UML构造形式语义,人们做了大量的工作.本文将讨论为UML的一种重要动态行为描述机制——状态机(statemachine)构造的形式化语义.状态机作为UML动态描述机制的重要组成部分,在描述系统及模型的动态行为时扮演着重要的角色.在一些对安全性要求较高的实时系统、嵌入式系统、分布
5、式系统以及调度系统中,是描述协议、控制单元等组件的常用而重要的手段.由于系统往往对这些组件的正确性要求较高,因此,为UML状态机构造形式化的语义就显得尤为迫切.因为这不仅有利于准确而无二义性地理解其所表示对象的行为,有利于系统的代码生成及优化,而且更有助于对系统的正确性和安全性进行形式化验证和证明.1UML状态机的状态项代数UML的状态包括简单状态、非并发复合状态和并发复合状态、初始状态、最终状态和子状态机状态、历史状态、同步状态.按如下状态分类:(1)基本状态,包括简单状态、初始状态和最终状态.初始状态和最终状态Ã收
6、稿日期:2001-04-17;修改日期:2001-11-02基金项目:国家自然科学基金资助项目(69931040)作者简介:蒋慧(1973－),女,重庆人,博士,讲师,现在清华大学计算机科学与技术系博士后流动站工作.主要研究领域为面向对象,软件工程,形式化方法;林东(1966－),男,江苏南京人,博士,副教授,主要研究领域为运筹学,计算机仿真,人工智能,决策支持;谢希仁(1931－),男,福建晋江人,教授,博士生导师,主要研究领域为计算机网络.蒋慧等:UML状态机的形式语义2245没有具体的状态名,只是用来表明进入或退
7、出某个状态.(2)或状态,即非并发复合状态.在某一时刻只能有一个子状态处于活跃状态.(3)与状态,即并发复合状态,有两个以上互不关联的(或正交的orthogonal)的逻辑与组件,称为区域(region).1.1状态项代数假设UML状态机的状态名空间为N,其中initial∈N,finial∈N,分别表示状态项s的初始状态和最终状ss态(如果有的话).整个状态机中变迁的集合用T表示.UML状态机的状态项代数定义如下:定义1.UML状态机的状态项集SA是由以下规则所定义的最小集合:(1)空状态∅:是一个状态项,它只表示状
8、态机初始状态的父状态;(2)基本状态:对每一n∈N,sp∈SA,是状态n的父状态的状态项,s=n:sp;entryAction;DoActivity;ExitAction则是一个状态项.n是该状态的状态名sˆ,EntryAction,DoActivity,ExitAction分别表示该状态的入口动作、活动和出口动作,由函数En
