UML活动图的操作语义

An Operational Semantics for UML Activity Diagrams

越来越多的系统采用UML(unified model language,统一建模语言)作为建模语言来进行系统分析和设计.UML活动图是UML语言中描述系统动态行为的一种方法,它广泛地运用于业务建模.由于UML活动图缺乏精确的动态语义,所以不利于对其所描述的系统进行形式化的分析、验证和确认.为解决这一问题,根据UML1.5语义文档,给出UML活动图的形式化操作语义.首先给出UML活动图的形式化的语法,然后详细地定义了活动图的格局和变迁,最后基于LTS给出了活动图的演绎规则.主要工作是:引入状态包的概念,使得描述更加清楚、完善;通过LTS定义活动图的操作语义,并详细阐述演绎规则,从而获得活动图的全局状态转移图,使定义的操作语义很容易地应用到形式化验证中.该语义覆盖了UML活动图的绝大部分特征,为对UML活动图进行模型检验奠定了基础.

More and more large systems are taking UML（unified model language） as requirements description language for system analysis and design,especially in those safety-critical systems.One of the most important dynamic behaviors specifying the mechanism of UML is the UML activity diagram,which is widely used for modeling of business.The UML activity diagram lacks strictly defined formal dynamic semantics.It is difficult using the UML activity diagram to make formal analysis,verification and assertation.An operational semantics for UML activity diagram is proposed according to UML1.5 specification documents.First,the formal syntax of UML activity diagram is provided.Then,the configuration and the transitions are defined in detail.Finally,the deduct rules of UML activity diagram are described based on the LTS.The main contributions are：Firstly,in order to get more precise and clearer description of formal semantics,the hierarchy of activity state is abandoned and instead the concept of state bag is introduced to define the configuration.Secondly,the LTS semantics and the detailed deduction rules of UML activity diagram are defined.The global state transition diagram can be computed from the LTS semantics conveniently.Therefore,the formal semantics is able to deal with most of the features of UML activity diagram and can be used in formal verification.