Detalhes do Documento

Dissertação (mestrado) - Pontifícia Universidade Católica de Minas Gerais, Programa de Pós-Graduação em Informática

Bibliografia: f. 86-89

A popularização dos sistemas gerenciadores de banco de dados (SGBDs) relacionais implicou no desenvolvimento de aplicações utilizando esta tecnologia para persistir dados de usuários. Isto possibilitou desde o desenvolvimento de aplicações usando um SGBD como um simples repositório de dados até sistemas complexos, em que todas as regras de negócio estão implementadas no SGBD através do uso de stored procedures. Como resultado surge a demanda de novas abordagens a fim de capturar erros específicos oriundos da integração entre essas aplicações e os bancos de dados. O propósito deste trabalho é apresentar uma metodologia para validar especificações da Structured Query Language (SQL) - implementadas como consultas ou stored procedures escritas em linguagem Transact-SQL - por meio do uso da verificação de modelos. A métodologia consiste na extração de um modelo formal que represente as operações de consultas da álgebra relacional e a lógica de programação estruturada das stored procedures. As especificações SQL são descritas como expressões em lógica temporal CTL adicionadas ao modelo como propriedades a serem verificadas. O código Transact-SQL, que implementa a especificação, está incorreto se o processo de verificação invalidar qualquer propriedade. Nesse caso, um contra-exemplo é exibido descrevendo os estados de erro. Palavras-chave: banco de dados. métodos formais. lógia temporal. testes de software. engenharia de software. álgebra relacional.

Abstract: The popularization of Relational database management systems (RDBMS) has implied the development of diferent 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. Keywords: databases. model check. CTL temporal logic. software tests. software engineering. relational algebra.