安全数据库顶层规范中SQL操作的形式化分析与验证  

Formal specification and verification for SQL operations in top level specification of secure database

作　　者：汪志鹏[1] 杨明慧[1] 陈兵[1] 王福[1] 

机构地区：[1]公安部第三研究所网络身份技术事业部,上海201204

出　　处：《计算机应用研究》2015年第6期1751-1756,共6页Application Research of Computers

基　　金：科研院所技术开发研究专项项目(2014EG53068);公安部科技强警基础工作专项项目(2014GABJC042)

摘　　要：介绍了安全数据库形式化顶层规范,定义了顶层规范中SQL操作的描述,在此基础上给出简单SQL操作的定义,并对其进行分析验证,最后将一般SQL操作的分析验证转换为多个简单SQL操作的分析验证。验证过程表明,该方法既对SQL操作作了完整清晰的描述,又简化了证明。This paper proposed a novel approach to solve the specification and verification issues towards SQL operations. Firstly, it formally defined the SQL operations in FTLS. Then, it gave the definitions of the simple SQL operations and pro- posed a method to verify them. Finally, this work transformed the verification of the SQL operations in FTLS to the verification of the component simple SQL operations. The process of verification shows that the approach makes a comprehensive specifica- tion of SQL operations and simplifies the verification procedure.

关 键 词：形式化顶层规范 安全数据库 SQL操作 形式化分析与验证 

分 类 号：TP311.13[自动化与计算机技术—计算机软件与理论]