UML状态机到B形式化规约的转换  

Transformation From UML State Machine to B Formal Specification

作　　者：肖健宇[1] 张德运[1] 董皓[1] 陈海诠[1] 

机构地区：[1]西安交通大学电子与信息工程学院

出　　处：《微电子学与计算机》2005年第8期80-84,共5页Microelectronics & Computer

基　　金：国家863网络安全管理与测评技术(8633010503)

摘　　要：文章研究在高可信软件工程中集成形式化方法。以软件设计的UML状态机模型为起点,将其转换为B形式化模型,然后在B工具环境中遵循B方法的精化原则和正确性验证方法,开发出可靠的实现模型。提出一套从UML状态机到B形式化规约的转换规则,涵盖UML基本状态图、分层状态图和并发状态图。实例分析表明,这套转换规则行之有效。Integration of formal method into high-confidence software engineering was studied. The UML state machine of software design model was first transformed into B formal specification. Then, in the B tool kit environment, the reliable implementation model was developed according to the refinement principle of B method and its correctness verification facility. A suit of transformation rules from UML state machine into B formal model were proposed, including UML basic state diagram, hierarchical state diagram and concurrent state diagram. Experiment showed that the proposed transformation rules were practical.

关 键 词：UML状态机 形式化方法 B方法 高可信软件工程 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]