基于XYZ/SE的软件部分正确性验证

• 作者: 刘曼霞 张锦 柳军飞 赵二群
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 形式化描述 部分正确性验证 结构化XYZ/E 国库信息处理系统
• 年，卷（期）: 2015,（14）
• 所属期刊栏目: 理论研究、研发设计
• 页码范围: 46-50
• 页数: 5页
• 分类号: TP391
• 字数: 4815字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.1308-0197

摘要

针对软件形式化描述和正确性验证研究中存在的问题，提出了基于XYZ/SE的统一框架研究该问题。在该框架下，基于逐步求精思路对软件进行抽象；对软件整体进行形式化描述和部分正确性验证；对抽象得到的软件各部分进行形式化描述和部分正确性验证；进行调整和验证，即：如果推导结果与预期不一致，则需要重写相关程序或者回溯检查推导过程是否存在错误，直至程序部分正确性得到验证为止。以国库信息处理系统为对象，分析了基于XYZ/SE的统一框架性能。分析表明，基于该框架能够对软件的不同抽象层次进行规范描述，实现从抽象（静态语义）到具体（动态语义）的平滑过渡。同时，基于XYZ/SE的统一框架也可以表示Hoare逻辑推演规则。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张锦	湖南师范大学数学与计算机科学学院	47	477	10.0	20.0
5	柳军飞	北京大学国家软件工程研究中心	3	6	1.0	2.0
6	赵二群	湖南大学信息科学与工程学院	3	3	1.0	1.0
7	刘曼霞	湖南大学信息科学与工程学院	1	0	0.0	0.0