Um estudo sobre verificação formal de sistemas concorrentes

Abstract

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.