Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2012. / Submitted by Albânia Cézar de Melo (albania@bce.unb.br) on 2012-10-18T16:28:45Z
No. of bitstreams: 1
2012_JoaoPauloCarvalhoColuQueiroz.pdf: 949010 bytes, checksum: 6c8c52f3b39f58d84a5780716ea83b12 (MD5) / Approved for entry into archive by Guimaraes Jacqueline(jacqueline.guimaraes@bce.unb.br) on 2012-10-24T11:08:41Z (GMT) No. of bitstreams: 1
2012_JoaoPauloCarvalhoColuQueiroz.pdf: 949010 bytes, checksum: 6c8c52f3b39f58d84a5780716ea83b12 (MD5) / Made available in DSpace on 2012-10-24T11:08:41Z (GMT). No. of bitstreams: 1
2012_JoaoPauloCarvalhoColuQueiroz.pdf: 949010 bytes, checksum: 6c8c52f3b39f58d84a5780716ea83b12 (MD5) / Este trabalho apresenta um estudo de metodologias para veri cação formal de aplicativos desenvolvidos em linguagens imperativas, em especial, na linguagem Java. Os formalismos teóricos mostrados incluem a Lógica de Hoare, usada para representar pro-
priedades de aplicações imperativas, e construções da linguagem de especi cação JML
(baseada na Lógica de Hoare), usada para especi car o comportamento esperado de apli-
cações codi cadas em Java. As ferramentas mostradas são o sistema Krakatoa, usado
para converter especi cações JML em obrigações de prova, e o ambiente interativo de provas Coq, usado para veri car obrigações de prova. Finalmente, exibe-se um estudo de
caso que utiliza o ferramental teórico e prático proposto. ______________________________________________________________________________ ABSTRACT / This work presents a study of methodologies to formally verify applications developed
with imperative languages, specially with the Java language. The theoretical formalisms
shown include Hoare Logic, which is used to sketch properties on imperative languages,
and JML constructions (based on Hoare Logic), which is a speci cation language used
to specify the expected behavior from Java programs. The tools shown are the Krakatoa
system, used to convert JML speci cations into proof obligations, and the Coq interactive proof environment, used to verify proof obligations. Finally, this paper presents a case study that employs the theoretical and practical proposed framework.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.unb.br:10482/11471 |
| Date | 06 July 2012 |
| Creators | Queiroz, João Paulo Carvalho Colu de |
| Contributors | Moura, Flávio Leonardo Cavalcanti de |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UnB, instname:Universidade de Brasília, instacron:UNB |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0094 seconds