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

Software partial correctness verification based on XYZ/SE

作　　者：张锦[1,2] 刘曼霞[2] 赵二群[2] 柳军飞[3] 

机构地区：[1]湖南师范大学数学与计算机科学学院,长沙410081 [2]湖南大学信息科学与工程学院,长沙410082 [3]北京大学国家软件工程研究中心,北京100871

出　　处：《计算机工程与应用》2015年第14期46-50,共5页Computer Engineering and Applications

基　　金：863重点课题(No.2009AA010314);国家自然科学基金(No.60901080)

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

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

分 类 号：TP391[自动化与计算机技术—计算机应用技术]