| Summary: | Made available in DSpace on 2014-12-17T15:47:56Z (GMT). No. of bitstreams: 1
DiegoHOS_DISSERT.pdf: 2899752 bytes, checksum: d3160b774efd6749eced9bb34d4a74cf (MD5)
Previous issue date: 2011-08-31 === Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior === 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++. === 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++.
|
|---|
