Skip to main content
Top

2016 | OriginalPaper | Chapter

An Approach for Verifying Educational Robots

Authors : Sidney Nogueira, Taciana Pontual Falcão, Alexandre Mota, Emanuel Oliveira, Itamar Moraes, Iverson Pereira

Published in: Formal Methods: Foundations and Applications

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference Anais do XXVI Simpósio Brasileiro de Informática na Educação (SBIE 2015) (2015) Anais do XXVI Simpósio Brasileiro de Informática na Educação (SBIE 2015) (2015)
4.
go back to reference 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 CrossRef 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 CrossRef
6.
go back to reference 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) 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)
7.
go back to reference Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. Wiley, New York (1999)MATH Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. Wiley, New York (1999)MATH
8.
go back to reference Nogueira, S., Sampaio, A., Mota, A.: Test generation from state based use case models. Formal Aspects Comput. 26(3), 441–490 (2014)MathSciNetCrossRefMATH Nogueira, S., Sampaio, A., Mota, A.: Test generation from state based use case models. Formal Aspects Comput. 26(3), 441–490 (2014)MathSciNetCrossRefMATH
10.
go back to reference 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 CrossRef 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 CrossRef
12.
go back to reference Papert, S.: A máquina das crianças. Artmed, Porto Alegre (1994) Papert, S.: A máquina das crianças. Artmed, Porto Alegre (1994)
13.
go back to reference Papert, S., Valente, J.A., Bitelman, B.: Logo: computadores e educação. Brasiliense (1980) Papert, S., Valente, J.A., Bitelman, B.: Logo: computadores e educação. Brasiliense (1980)
14.
go back to reference Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1998) Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1998)
15.
go back to reference Roscoe, A.W.: Understanding Concurrent System. Springer, Heidelberg (2011) Roscoe, A.W.: Understanding Concurrent System. Springer, Heidelberg (2011)
16.
go back to reference Roscoe, A.W., Hopkins, D.: SVA, a tool for analysing shared-variable programs. Proc. AVoCS 2007, 177–183 (2007) Roscoe, A.W., Hopkins, D.: SVA, a tool for analysing shared-variable programs. Proc. AVoCS 2007, 177–183 (2007)
17.
go back to reference University of Oxford: FDR3 Web Site, May 2015 University of Oxford: FDR3 Web Site, May 2015
Metadata
Title
An Approach for Verifying Educational Robots
Authors
Sidney Nogueira
Taciana Pontual Falcão
Alexandre Mota
Emanuel Oliveira
Itamar Moraes
Iverson Pereira
Copyright Year
2016
DOI
https://doi.org/10.1007/978-3-319-49815-7_4

Premium Partner