Uma abordagem para tradução de uma linguagem de programação de robôs para um modelo formal

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.