摘要： 采用定理证明和逆向工程的方法，对Web应用中的数据库交互行为进行验证。使用Z规格说明描述需求模型，根据数据库交互的源代码和转换规则得到实现模型。从实现模型中获取Web应用的相关性质，通过Z/EVES定理证明器验证这些性质是否在需求模型的 Z规格说明中得到满足。在此基础上，设计该方法的验证框架，并开发相应的原型系统。通过图书馆数据库管理系统实例证明该方法的有 效性。

关键词: 形式验证, Z规格说明, 数据库交互, 逆向工程, 定理证明

Abstract: This paper introduces theorem proving method and reverse engineering method to verify database interactions of Web application. Z specification considered as the requirement model is used to describe user’s requirements. According to the proposed transformation rules, abstract database interactions from source code of Web application as implementation model, then transform these codes to Z specification. Z/EVES is used to prove whether the implementation model conforms to its properties which are written as theorems. On this basis, it designs the verify framework for the proposed method and the prototype is developed. The library database management system shows the validity of this method.

Key words: formal verification, Z specification, database interaction, reverse engineering, theorem proving

中图分类号: 

• TP311