Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/74655
Título: | A deductive reasoning approach for database applications using verification conditions |
Autor(es): | Alam, Imran Halder, Raju Pinto, Jorge Sousa |
Palavras-chave: | Database languages Deductive reasoning Formal verification Verification conditions |
Data: | Mai-2021 |
Editora: | Elsevier 1 |
Revista: | Journal of Systems and Software |
Resumo(s): | Deductive verification has gained paramount attention from both academia and industry. Although intensive research in this direction covers almost all mainstream languages, the research community has paid little attention to the verification of database applications. This paper proposes a comprehensive set of Verification Conditions (VCs) generation techniques from database programs, adapting Symbolic Execution, Conditional Normal Form, and Weakest Precondition. The validity checking of the generated VCs for a database program determines its correctness w.r.t. the annotated database properties. The developed prototype DBverify based on our theoretical foundation allows us to instantiate VC generation from PL/SQL codes, yielding to detailed performance analysis of the three approaches under different circumstances. With respect to the literature, the proposed approach shows its competence to support crucial SQL features (aggregate functions, nested queries, NULL values, and set operations) and the embedding of SQL codes within a host imperative language. For the chosen set of benchmark PL/SQL codes annotated with relevant properties of interest, our experiment shows that only 38% of procedures are correct, while 62% violate either all or part of the annotated properties. The primary cause for the latter case is mostly due to the acceptance of runtime inputs in SQL statements without proper checking. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/74655 |
DOI: | 10.1016/j.jss.2020.110903 |
ISSN: | 0164-1212 |
e-ISSN: | 1873-1228 |
Versão da editora: | https://www.sciencedirect.com/science/article/pii/S0164121220302934#! |
Arbitragem científica: | yes |
Acesso: | Acesso restrito UMinho |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
2021_JSS_2021.pdf Acesso restrito! | 3,68 MB | Adobe PDF | Ver/Abrir |