|
Title:
|
VALIDATING SQL CODE USING SYMBOLIC MODEL CHECKING |
|
Author(s):
|
Rodrigo Diana, Mark Song, Humberto Torres |
|
ISBN:
|
978-989-8533-06-7 |
|
Editors:
|
Hans Weghorn, Leonardo Azevedo and Pedro Isaías |
|
Year:
|
2011 |
|
Edition:
|
Single |
|
Keywords:
|
Database; Model Check; Temporal Logic; Software Testing; Software Engineering; Relational Algebra |
|
Type:
|
Full Paper |
|
First Page:
|
19 |
|
Last Page:
|
26 |
|
Language:
|
English |
|
Cover:
|
|
|
Full Contents:
|
click to dowload 
|
|
Paper Abstract:
|
The popularization of Relational database management systems (RDBMS) has implied the development of different integrated applications. It makes it possible to develop a simple data repository application or a complex system in which every business rule is implemented, for example, through stored procedures. Therefore, new approaches are demanded in order to capture specific errors as a consequence of integrations between applications and databases. The propose of this paper is to present an approach to validate SQL specifications - implemented as Transact-SQL queries or stored procedures - using model checking. The method consists of extracting a model that represents the relational operations. The SQL specifications are described as CTL logic expressions and added to the model as properties to be checked. If the verification process invalidates a property then the Transact-SQL code implementing the specification is incorrect. In this case, a counterexample is presented describing the error. |
|
|
|
|
|
|
