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

计算机工程与应用 ›› 2015, Vol. 51 ›› Issue (14): 46-50.

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

张锦1，2，刘曼霞2，赵二群2，柳军飞3

1.湖南师范大学数学与计算机科学学院，长沙 410081
2.湖南大学信息科学与工程学院，长沙 410082
3.北京大学国家软件工程研究中心，北京 100871

出版日期:2015-07-15 发布日期:2015-08-03

Software partial correctness verification based on XYZ/SE

ZHANG Jin1，2, LIU Manxia2, ZHAO Erqun2, LIU Junfei3

1.College of Mathematics and Computer Science, Hunan Normal University, Changsha 410081, China
2.College of Information Science and Engineering, Hunan University, Changsha 410082, China
3.National Engineering Research Center of Software Engineering, Peking University, Beijing 100871, China

Online:2015-07-15 Published:2015-08-03

摘要/Abstract

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

关键词: 形式化描述, 部分正确性验证, 结构化XYZ/E, 国库信息处理系统

Abstract: To the problems on software formal description and partial correctness verification, a unified frame based on XYZ/SE is proposed. The unified frame includes four steps. Software is abstracted based on stepwise idea. It uses XYZ/SE to finish formal description and partial correctness verification of whole software. It uses XYZ/SE to finish formal description and partial correctness verification of each component of software. It adjusts and validates previous inference. If inferred results are different from anticipated conclusion, related program should be rewritten or inferring process should be checked to make sure possible wrong until partial correctness can be proved. In order to analyze the practicability of the unified frame, Treasury Information Process System （TIPS） is selected as research object. Analytical results show that XYZ/SE has the capability to describe formally different abstract level of software and realize smooth transition from static semantics to dynamic semantics. Meanwhile, the unified frame based on XYZ/SE can express inferring rules of Horse.

Key words: formal description, partial correctness verification, structural XYZ/SE, treasury information process system

张锦1，2，刘曼霞2，赵二群2，柳军飞3. 基于XYZ/SE的软件部分正确性验证[J]. 计算机工程与应用, 2015, 51(14): 46-50.

ZHANG Jin1，2, LIU Manxia2, ZHAO Erqun2, LIU Junfei3. Software partial correctness verification based on XYZ/SE[J]. Computer Engineering and Applications, 2015, 51(14): 46-50.

[1]	邓志丹，杨海燕，吴际. 一种约束求解的Web应用测试数据生成与筛选方法[J]. 计算机工程与应用, 2016, 52(18): 214-221.
[2]	汪漪^1，2，李皓^1，2，李晓¹，周俊林³，王磊¹. 多语种构件模型的研究与实现[J]. 计算机工程与应用, 2010, 46(14): 143-147.
[3]	谢兄，张维石. 构件适应和组装的形式化语义描述[J]. 计算机工程与应用, 2007, 43(21): 36-39.
[4]	蔡剑红李德仁. 多空间尺度下顾及不确定性的投影模型研究[J]. 计算机工程与应用, 2007, 43(14): 77-80.