UML状态机的形式语义

摘要

许多大型系统在进行分析和设计时,均采用UML作为需求描述语言,尤其是一些对安全性要求较高的系统,更是广泛采用UML的动态行为描述机制--状态机来描述协议及控制机制.但是,由于UML没有形式化的动态语义,不利于对其所描述的需求进行形式化验证和证明.为了解决这一问题,采用以下方法为UML状态机构建形式语义.把UML状态机中的状态映射到一种项代数上,用归纳的状态项表示状态机的状态.然后,把状态项映射到一种加标记的变迁系统LTS上,LTS-状态是状态机的状态项,LTS-变迁是UML状态机的微步.最后,用Plotkin风格的结构操作语义SOS(structural operational semantics)规则归纳地给出满足组合性的UML状态机语义.此方法既是对一些经典Statechart形式化方法的综合,又针对UML状态机的特点作了创新,使状态项能够动态地描述任意时刻UML状态机的配置树,简化LTS的标记,同时,结构化的语义规则更为形式化验证奠定了基础.