Um estudo sobre verificação formal de sistemas concorrentes

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorMoura, Flávio Leonardo Cavalcanti de-
Autor(es): dc.creatorQueiroz, João Paulo Carvalho Colu de-
Data de aceite: dc.date.accessioned2024-07-22T13:05:19Z-
Data de disponibilização: dc.date.available2024-07-22T13:05:19Z-
Data de envio: dc.date.issued2012-10-24-
Data de envio: dc.date.issued2012-10-24-
Data de envio: dc.date.issued2012-10-24-
Data de envio: dc.date.issued2012-07-06-
Fonte completa do material: dc.identifierhttp://repositorio.unb.br/handle/10482/11471-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/817570-
Descrição: dc.descriptionDissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2012.-
Descrição: dc.descriptionEste 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.descriptionThis 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.formatapplication/pdf-
Direitos: dc.rightsAcesso Aberto-
Palavras-chave: dc.subjectLinguagem de programação (Computadores)-
Palavras-chave: dc.subjectJava (Linguagem de programação de computador)-
Título: dc.titleUm estudo sobre verificação formal de sistemas concorrentes-
Aparece nas coleções:Repositório Institucional – UNB

Não existem arquivos associados a este item.