形式化方法B的精化

• 作者: 覃征 邵利平 高洪江 鹿蕾
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 形式化方法 广义代换 抽象机 前向精化 反向精化 证明义务
• 年，卷（期）: 2007,（9）
• 所属期刊栏目: 博士论文
• 页码范围: 49-51
• 页数: 3页
• 分类号: TP311
• 字数: 3428字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2007.09.017

摘要

形式化方法B支持从抽象规约到实现的完整的开发过程,用于开发安全关键的软件系统.给出了B方法精化的定义后,介绍了抽象机的精化过程与方法,结合实例分析了仅使用前向精化的普通精化规则的不完整性,通过引入反向精化提供了完备的精化理论,二者联合起来能够证明任何正确的精化.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	覃征	西安交通大学电子与信息工程学院	158	2651	25.0	46.0
5	邵利平	西安交通大学电子与信息工程学院	25	263	11.0	15.0
6	高洪江	西安交通大学电子与信息工程学院	7	101	6.0	7.0