摘要
文章研究在高可信软件工程中集成形式化方法。以软件设计的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.
出处
《微电子学与计算机》
CSCD
北大核心
2005年第8期80-84,共5页
Microelectronics & Computer
基金
国家863网络安全管理与测评技术(8633010503)
关键词
UML状态机
形式化方法
B方法
高可信软件工程
UML state machine, Formal method, B-method, High-confidence software engineering
