Use este identificador para citar ou linkar para este item: https://repository.ufrpe.br/handle/123456789/703
Título: Uma abordagem para tradução de uma linguagem de programação de robôs para um modelo formal
Autor: Pereira, Iverson Luís
Endereco Lattes do autor: http://lattes.cnpq.br/1186672408246777
Orientador: Nogueira, Sidney de Carvalho
Endereco Lattes do orientador : http://lattes.cnpq.br/9171224058305522
Palavras-chave: Engenharia de software;Software - Testes;Software - Desenvolvimento
Data do documento: 2018
Citação: PEREIRA, Iverson Luís. Uma abordagem para tradução de uma linguagem de programação de robôs para um modelo formal. 2018. 88 f. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação) - Departamento de Computação, Universidade Federal Rural de Pernambuco, Recife, 2018.
Abstract: There is an increasing interest in virtual robot programming environments for educational purposes in recent years. These environments are an alternative to the use of real robots, which have a high acquisition value. Automatic verification of robot programs is a demand of students and teachers that expect to have fast and automatic feed back about the correctness of robot programs.However,no free software provides an automatic verification of virtual robot programs. This work proposes an approach for the automatic verification of virtual robot programs authored in the educational language called ROBO. We propose a compiler that reads programs written in ROBO and translates its source code into a formal notation called CSP (Communicating Sequential Processes), which is the input to a model checking tool called FDR (FailuresDivergences Refinement). The compiler was implemented using the facilities of the Spoofax framework, which is used to define a parser for the ROBO language and a set of translation rules from ROBO to CSP. This work removes a limitation of our previous verification approach that does not perform the verification of ROBO programs containing variables and procedures. A significant contribution is the extension of the verification approach to allow the automatic analysis of ROBO programs with variables and procedures.The extension consists of the modification of the compiler Grammar by the inclusion of variables and procedures and the inclusion of translation rules that define the formal semantics for the elements added into the grammar.Moreover, the work proposes a tool that makes transparent the translation process from ROBO to CSP and the automatic verification using FDR.We validate the approach using the proposed tool to verify the behavior of a ROBO program with variables and procedures.
Resumo: O interesse por ambientes de programação de robôs virtuais para fins educacionais tem crescido nos últimos anos. Estes ambientes são uma alternativa para o uso de robôs reais que possuem um alto custo de aquisição. No entanto, não existem ambientes gratuitos que oferecem mecanismos automatizados para verificação dos programas de robôs virtuais, o que impossibilita que alunos e professores tenham um feedback rápidoeautomáticosobreofuncionamentodosprogramas.Estetrabalhopropõe umaabordagemdeverificaçãoautomáticadeprogramasderobôsvirtuaisescritosna linguagemeducacionalROBO.DesenvolvemosumcompiladorquelêprogramasescritosemROBOetraduzosprogramasparaumanotaçãoformalchamadaCSP(Communicating Sequential Processes), que é a entrada para uma ferramenta de verificação automática de modelos chamada FDR (Failures-Divergences Refinement). As fases da compilação foram implementadas usando a plataforma Spoofax, onde definimos a gramática da linguagem ROBO e especificamos regras de tradução de ROBO para CSP. Estetrabalhoremoveumalimitaçãodanossaabordagemanteriordeverificação que não permite a análise de programas ROBO contendo variáveis e procedimentos. Uma importante contribuição deste trabalho é a extensão da abordagem de verificação para permitir a análise automática de programas ROBO com variáveis e procedimentos. A extensão consiste na modificação da gramática do compilador pela inclusão de variáveis e procedimentos e na inclusão de novas regras de tradução que definem a semântica formal para os elementos adicionados na gramática. O trabalho propõe uma ferramenta que torna transparente o processo de tradução de ROBO para CSP e a verificação automática usando FDR. Validamos a abordagem utilizando a ferramenta proposta para verificar o comportamento de um programa ROBO com variáveis e procedimentos.
URI: https://repository.ufrpe.br/handle/123456789/703
Aparece nas coleções:TCC - Bacharelado em Ciência da Computação (Sede)

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
tcc_Iverson Luís Pereira.pdf2,13 MBAdobe PDFVisualizar/Abrir


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.