Joker: um realizador de desenhos animados para linguagens formais

Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However, there are many resistance in adopting this software development approach. The main reason is the scarcity of adequate, easy to use, and useful tools. Developers typically write code and test it. These tests usually consist of executing the program and checking its output against its requirements. This, however, is not always an exhaustive discipline. On the other side, using formal methods one might be able to investigate the system s properties further. Unfortunately, specification languages do not always have tools like animators or simulators, and sometimes there are no friendly Graphical User Interfaces. On the other hand, specification languages usually have a compiler which normally generates a Labeled Transition System (LTS). This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B, CSP, and Z. However, using a LTS in a specified XML format, it is possible to animate further languages. Additionally, the tool provides traces visualization, the choices the user did, in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it, as the developers do for programming languages, such as Java and C++.

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior

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++.