Research of Formal Verification for SQL Operations in Top Level Specification of a Secure Database
A high security level DBMS requires a formal specification and verification on the security model and top level specification design. The specification and verification towards SQL operations are important especially. In this paper, based on the security model and top level specification, the authors propose a novel approach to solve the specification and verification issues towards SQL operations. Firstly, they formally define the SQL operations in FTLS then, they give the definitions of the simple SQL operations and propose a method to verify those simple SQL operations finally, they transform the verification of the SQL operations in FTLS to the verification of the component simple SQL operations.