Uma técnica para modelagem e verificação de programas JAVA concorrentes auxiliada por anotações de código.

Detalhes bibliográficos
Ano de defesa: 2006
Autor(a) principal: OLIVEIRA, Elthon Allex da Silva.
Orientador(a): Não Informado pela instituição
Banca de defesa: Não Informado pela instituição
Tipo de documento: Dissertação
Tipo de acesso: Acesso aberto
Idioma: por
Instituição de defesa: Universidade Federal de Campina Grande
Brasil
Centro de Engenharia Elétrica e Informática - CEEI
PÓS-GRADUAÇÃO EM CIÊNCIA DA COMPUTAÇÃO
UFCG
Programa de Pós-Graduação: Não Informado pela instituição
Departamento: Não Informado pela instituição
País: Não Informado pela instituição
Palavras-chave em Português:
Link de acesso: http://dspace.sti.ufcg.edu.br:8080/jspui/handle/riufcg/11693
Resumo: Métodos formais vêm sendo utilizados muito hoje em dia em projetos de desenvolvimento em que há uma grande exigência de que o software se comporte exatamente conforme esperado. Entretanto, os projetos que fazem uso de métodos formais se limitam aos poucos projetos que estão dispostos a investir em recursos humanos capacitados. Neste trabalho é apresentada uma técnica desenvolvida para viabilizar a inclusão de métodos formais, mais especificamente a técnica de verificação de modelos (model checking), nos processos de desenvolvimento de software concorrente orientado a objetos. É então definida uma linguagem de descrição comportamental capaz de descrever e abstrair o comportamento de programas orientados a objetos com múltiplas linhas de execução. Tal linguagem, escrita junto ao código na forma de linguagem de anotação, atua como mecanismo de abstração do programa a ser verificado. Por ser uma linguagem semelhante a uma linguagem de programação, o programador é quem modela seu próprio código, dispensando o especialista que seria necessário para modelagem formal do sistema. Além disso, por ser de anotação, ameniza o problema da sincronização entre o modelo e o sistema modelado. Os modelos descritos usando a linguagem de descrição comportamental são então traduzidos para uma linguagem formal executável existente. A partir deste modelo formal e das propriedades especificadas a serem verificadas, é realizada a verificação de modelos utilizando um verificador de modelos. O desenvolvedor permanece em contato apenas com as anotações e os resultados obtidos no processo de verificação. O restante do processo ocorre de forma totalmente escondida do usuário, numa caixa preta.