Joker: um realizador de desenhos animados para linguagens formais

AUTOR(ES)
FONTE

IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia

DATA DE PUBLICAÇÃO

31/08/2011

RESUMO

Usando métodos formais, o desenvolvedor pode aumentar a confiabilidade e corretude do software. Além disso, o desenvolvedor pode concentrar-se mais nos requisitos funcionais. Porém há muita resistência em se adotar essa abordagem de desenvolvimento de software. A razão principal e a escassez de suporte ferramental adequado, útil e de fácil utilização. Os desenvolvedores normalmente escrevem o código e o testam. Estes testes geralmente consistem em checar se as saídas estão de acordo com os requisitos. Isto, contudo, nem sempre e possível de maneira exaustiva. Por outro lado, usando Métodos Formais um desenvolvedor e capaz de investigar profundamente as propriedades do sistema. Infelizmente, linguagens de especificação formal nem sempre possuem ferramentas como animador ou simulador e às vezes não há interfaces gráficas amigáveis. Porém, algumas dessas ferramentas possuem um compilador, que gera um Sistema de Transições Rotuladas (LTS). A proposta deste trabalho é desenvolver um aplicativo que fornece animação gráfica para especificações formais usando o LTS como entrada. O aplicativo inicialmente suporta as as linguagens B, CSP e Z. Usando o LTS em um formato XML especificado é possível animar outras linguagens formais. Adicionalmente a ferramenta disponibiliza visualização de traces, escolhas feitas pelo usuário, em um formato de árvore gráfica. A intenção é melhorar a compreensão de uma especificação, fornecendo informações sobre erros e animando-a, como os desenvolvedores fazem com linguagens de programação como Java e C++.

ASSUNTO(S)

interface gráfica animação java especificação formal métodos formais. sistemas de computacao graphical user interface animation java formal specifications formal methods.

Documentos Relacionados