Atenção: Todas as denúncias são sigilosas e sua identidade será preservada.
Os campos nome e e-mail são de preenchimento opcional
Metadados | Descrição | Idioma |
---|---|---|
Autor(es): dc.contributor | Moura, Flávio Leonardo Cavalcanti de | - |
Autor(es): dc.creator | Queiroz, João Paulo Carvalho Colu de | - |
Data de aceite: dc.date.accessioned | 2024-07-22T13:05:19Z | - |
Data de disponibilização: dc.date.available | 2024-07-22T13:05:19Z | - |
Data de envio: dc.date.issued | 2012-10-24 | - |
Data de envio: dc.date.issued | 2012-10-24 | - |
Data de envio: dc.date.issued | 2012-10-24 | - |
Data de envio: dc.date.issued | 2012-07-06 | - |
Fonte completa do material: dc.identifier | http://repositorio.unb.br/handle/10482/11471 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/capes/817570 | - |
Descrição: dc.description | Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2012. | - |
Descrição: dc.description | 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 | - |
Descrição: dc.description | 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. | - |
Formato: dc.format | application/pdf | - |
Direitos: dc.rights | Acesso Aberto | - |
Palavras-chave: dc.subject | Linguagem de programação (Computadores) | - |
Palavras-chave: dc.subject | Java (Linguagem de programação de computador) | - |
Título: dc.title | Um estudo sobre verificação formal de sistemas concorrentes | - |
Aparece nas coleções: | Repositório Institucional – UNB |
O Portal eduCAPES é oferecido ao usuário, condicionado à aceitação dos termos, condições e avisos contidos aqui e sem modificações. A CAPES poderá modificar o conteúdo ou formato deste site ou acabar com a sua operação ou suas ferramentas a seu critério único e sem aviso prévio. Ao acessar este portal, você, usuário pessoa física ou jurídica, se declara compreender e aceitar as condições aqui estabelecidas, da seguinte forma: