Please use this identifier to cite or link to this item: https://repositorio.ufrn.br/handle/123456789/18024
Full metadata record
DC FieldValueLanguage
dc.contributor.advisorOliveira, Marcel Vinicius Medeirospt_BR
dc.contributor.authorSouza, Diego Henrique Oliveira dept_BR
dc.date.accessioned2014-12-17T15:47:56Z-
dc.date.available2012-01-13pt_BR
dc.date.available2014-12-17T15:47:56Z-
dc.date.issued2011-08-31pt_BR
dc.identifier.citationSOUZA, Diego Henrique Oliveira de. Joker: um realizador de desenhos animados para linguagens formais. 2011. 122 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Natal, 2011.por
dc.identifier.urihttps://repositorio.ufrn.br/jspui/handle/123456789/18024-
dc.description.abstractUsing 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++.eng
dc.description.sponsorshipCoordenação de Aperfeiçoamento de Pessoal de Nível Superiorpt_BR
dc.formatapplication/pdfpor
dc.languageporpor
dc.publisherUniversidade Federal do Rio Grande do Nortepor
dc.rightsAcesso Abertopor
dc.subjectInterface Gráficapor
dc.subjectAnimaçãopor
dc.subjectJavapor
dc.subjectEspecificação formalpor
dc.subjectMétodos formais.por
dc.subjectGraphical User Interfaceeng
dc.subjectAnimationeng
dc.subjectJavaeng
dc.subjectFormal Specificationseng
dc.subjectFormal Methods.eng
dc.titleJoker: um realizador de desenhos animados para linguagens formaispor
dc.typemasterThesispor
dc.publisher.countryBRpor
dc.publisher.initialsUFRNpor
dc.publisher.programPrograma de Pós-Graduação em Sistemas e Computaçãopor
dc.contributor.authorIDpor
dc.contributor.authorLatteshttp://lattes.cnpq.br/7244077194054059por
dc.contributor.advisorIDpor
dc.contributor.advisorLatteshttp://lattes.cnpq.br/1756952696097255por
dc.contributor.referees1Mota, Alexandre Cabralpt_BR
dc.contributor.referees1IDpor
dc.contributor.referees1Latteshttp://lattes.cnpq.br/2794026545404598por
dc.contributor.referees2Leite, Jair Cavalcantipt_BR
dc.contributor.referees2IDpor
dc.contributor.referees2Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4782411P6por
dc.description.resumoUsando 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++.por
dc.publisher.departmentCiência da Computaçãopor
dc.subject.cnpqCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAOpor
Appears in Collections:PPGSC - Mestrado em Sistemas e Computação

Files in This Item:
File Description SizeFormat 
DiegoHOS_DISSERT.pdf2,83 MBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.