Joker: Um Framework de Animação para Especificações Formais
Métodos Formais, Circus, Animação
Muitas ferramentas provém suporte a métodos formais em todo o processo de desenvolvimento. No entanto, na maioria das vezes elas não são fáceis de usar e tem uma curva de aprendizagem significativa. Isso cria uma resistência em adotar a abordagem. Às vezes, apesar de ter um compilador que é capaz de gerar um sistema de transições rotuladas (LTS) a partir da especificação, a linguagem não fornece um animador. Essa ferramenta pode ser usada para melhorar a compreensão de uma especificação, pois pode ser usada para prototipar o sistema. A ferramenta que apresentamos nesta dissertação, Joker, visa animar qualquer linguagem formal usando apenas o seu LTS como entrada. Já é capaz de animar Lotos, B, CSP e Z. Nós apresentamos as funcionalidades da ferramenta e, mais importante, como ele pode ser adaptado para outras linguagens formais.