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

• 作者: 张德运 肖健宇 董皓 陈海诠
• 来源期刊: 微电子学与计算机
• 关键词: UML状态机 形式化方法 B方法 高可信软件工程
• 年，卷（期）: 2005,（8）
• 页码范围: 80-84
• 页数: 5页
• 分类号: TP311.1
• 语种: 中文
• DOI: 10.3969/j.issn.1000-7180.2005.08.021

摘要

文章研究在高可信软件工程中集成形式化方法.以软件设计的UML状态机模型为起点,将其转换为B形式化模型,然后在B工具环境中遵循B方法的精化原则和正确性验证方法,开发出可靠的实现模型.提出一套从UML状态机到B形式化规约的转换规则,涵盖UML基本状态图、分层状态图和并发状态图.实例分析表明,这套转换规则行之有效.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张德运	西安交通大学电子与信息工程学院	184	2190	23.0	37.0
2	肖健宇	西安交通大学电子与信息工程学院	13	83	6.0	8.0
4	陈海诠	西安交通大学电子与信息工程学院	8	67	5.0	8.0
5	董皓	西安交通大学电子与信息工程学院	12	83	6.0	9.0