Abstract
Virtual robot programming environments provide a visual interface for programming and simulating educational robots. Nowadays, simulation is the only way to assess the robot behaviour inside such environments, as there is no approach that supports the automatic analysis of the correctness of robot programs. This paper introduces an automatic approach for verifying robot programs written in the educational programming language ROBO. We give semantics for ROBO programs in the setting of CSP process algebra and automatically verify the properties of the programs using the FDR refinement checker. The verification approach has been defined considering programming exercises proposed in the literature on educational robotics. We illustrate the approach using sample programs written in ROBO and discuss how to integrate such an approach with educational tools.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Anais do XXVI Simpósio Brasileiro de Informática na Educação (SBIE 2015) (2015)
Online judge, February 2016. https://en.wikipedia.org/wiki/Online_judge
RoboMind FURB (2016). http://robolab.inf.furb.br/
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_13
Kitchen, R., Amsterdam, U.V.: RoboMind. http://robomind.net/
Lessa, V., Forigo, F., Teixeira, A., Licks, G.P.: Programação de computadores e robótica educativa na escola: tendências evidenciadas nas produções do workshop de informática na escola. In: Anais do Workshop de Informática na Escola, vol. 21, p. 92 (2015)
Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. Wiley, New York (1999)
Nogueira, S., Sampaio, A., Mota, A.: Test generation from state based use case models. Formal Aspects Comput. 26(3), 441–490 (2014)
Nogueira, S., et al.: Exercises Catalog and Paper Samples, August 2016. http://bit.ly/2aYR2Q4
Nogueira, S., Araujo, H.L.S., Araujo, R.B.S., Iyoda, J., Sampaio, A.: Automatic generation of test cases and test purposes from natural language. In: Cornélio, M., Roscoe, B. (eds.) SBMF 2015. LNCS, vol. 9526, pp. 145–161. Springer, Heidelberg (2016). doi:10.1007/978-3-319-29473-5_9
Oracle: Java JSE, August 2016. http://www.oracle.com/
Papert, S.: A máquina das crianças. Artmed, Porto Alegre (1994)
Papert, S., Valente, J.A., Bitelman, B.: Logo: computadores e educação. Brasiliense (1980)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1998)
Roscoe, A.W.: Understanding Concurrent System. Springer, Heidelberg (2011)
Roscoe, A.W., Hopkins, D.: SVA, a tool for analysing shared-variable programs. Proc. AVoCS 2007, 177–183 (2007)
University of Oxford: FDR3 Web Site, May 2015
Wing, J.M.: Computational thinking. Commun. ACM 49(3), 33–35 (2006)
Acknowledgements
This research project is supported by CNPq under grant 442859/2014-7.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Nogueira, S., Falcão, T.P., Mota, A., Oliveira, E., Moraes, I., Pereira, I. (2016). An Approach for Verifying Educational Robots. In: Ribeiro, L., Lecomte, T. (eds) Formal Methods: Foundations and Applications. SBMF 2016. Lecture Notes in Computer Science(), vol 10090. Springer, Cham. https://doi.org/10.1007/978-3-319-49815-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-49815-7_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-49814-0
Online ISBN: 978-3-319-49815-7
eBook Packages: Computer ScienceComputer Science (R0)