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

摘要

针对软件形式化描述和正确性验证研究中存在的问题，提出了基于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 descrip-tion 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.