Verificação eficiente de robôs educacionais

Abstract

Educational robotics is an area of growing interest within educational institutions. Due to it's low cost, program environments for virtual robots have been developed to support the teaching of computing, programming and robotics concepts. The main debug tool available in such environments is the simulation of the robot within a virtual map. Debugging is performed by observing the robot moving across the map: it is not possible to analyze automatically if a program will manage to conclude a specific objective. Approaches to automatically analyze virtual robots are an important teaching tool for an eficient and accurate evaluation of robots. The objective of this project is to improve an automatic verification approach of robot programs. This approach translates programs in the ROBO language to the formal notation CSP and uses the FDR model checker to automatically analyze the program's behavior. The result returned by the model checker is used to inform if the analyzed program has the expected behavior. The main improvement proposed by this project is the implementation of a ROBO to CSP translator that generates a more eficient CSP model to be analyzed, if compared to the model produced by the previous translator. We could observe, through empirical evaluation, a significant reduction in the time to analyze the CSP models obtained from the new translator. The proposed translator presents an almost constant analysis time for the maps considered in the empirical evaluation, while analysis time of the models produced by the previous translator shows an exponential growth in relation to the map's size where the program is analyzed. Another contribution of this work is that the new translator accepts ROBO programs with any command of the language, while the previous translator could only deal with a subset.