Skip to main content
SpringerLink
Log in

Modelling and Verification of Timed Robotic Controllers

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10510))

Included in the following conference series:

Abstract

Designing robotic systems can be very challenging, yet controllers are often specified using informal notations with development driven primarily by simulations and physical experiments, without relation to abstract models of requirements. The ability to perform formal analysis and replicate results across different robotic platforms is hindered by the lack of well-defined formal notations. In this paper we present a timed state-machine based formal notation for robotics that is informed by current practice. We motivate our work with an example from swarm robotics and define a compositional CSP-based discrete timed semantics suitable for refinement. Our results support verification and, importantly, enable rigorous connection with sound simulations and deployments.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://www.cs.york.ac.uk/circus/RoboCalc.

  2. 2.

    www.eclipse.org/sirius and www.eclipse.org/xtext.

References

  1. Chen, J., Gauci, M., Gross, R.: A strategy for transporting tall objects with a swarm of miniature mobile robots. In: 2013 IEEE International Conference on Robotics and Automation (ICRA), pp. 863–869, May 2013

    Google Scholar 

  2. Liu, W., Winfield, A.F.T.: Modeling and optimization of adaptive foraging in swarm robotic systems. Int. J. Robot. Res. 29(14), 1743–1760 (2010)

    Article  Google Scholar 

  3. Li, W., Miyazawa, A., Ribeiro, P., Cavalcanti, A.L.C., Woodcock, J.C.P., Timmis, J.: From formalised state machines to implementation of robotic controllers. In: Chong, N.-Y., Cho, Y.-J. (eds.) DARS 2016. Springer, London (2016)

    Google Scholar 

  4. Schneider, S.: Concurrent and Real-time Systems: the CSP Approach. Worldwide Series in Computer Science. Wiley, Chichester (2000)

    Google Scholar 

  5. Sherif, A., Cavalcanti, A.L.C., He, J., Sampaio, A.C.A.: A process algebraic framework for specification and validation of real-time systems. Formal Aspects Comput. 22(2), 153–191 (2010)

    Article  MATH  Google Scholar 

  6. Woodcock, J.C.P., Davies, J.: Using Z-Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

  7. Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, Heidelberg (2011)

    MATH  Google Scholar 

  8. Woodcock, J.: The miracle of reactive programming. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 202–217. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14521-6_12

    Chapter  Google Scholar 

  9. 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

    Chapter  Google Scholar 

  10. Hilder, J.A., Owens, N.D.L., Neal, M.J., Hickey, P.J., Cairns, S.N., Kilgour, D.P.A., Timmis, J., Tyrrell, A.M.: Chemical detection using the receptor density algorithm. IEEE Trans. Syst. Man Cybern. C Appl. Rev. 42(6), 1730–1741 (2012)

    Article  Google Scholar 

  11. Dixon, C., Winfield, A.F.T., Fisher, M., Zeng, C.: Towards temporal verification of swarm robotic systems. Robot. Auton. Syst. 60(11), 1429–1441 (2012)

    Article  Google Scholar 

  12. Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21–41. Springer, Cham (2015). doi:10.1007/978-3-319-14806-9_2

    Google Scholar 

  13. Nouyan, S., Gross, R., Bonani, M., Mondada, F., Dorigo, M.: Teamwork in self-organized robot colonies. IEEE Trans. Evol. Comput. 13(4), 695–711 (2009)

    Article  Google Scholar 

  14. Pini, G., Brutschy, A., Scheidler, A., Dorigo, M., Birattari, M.: Task partitioning in a robot swarm: object retrieval as a sequence of subtasks with direct object transfer. Artif. Life 20(3), 291–317 (2014)

    Article  Google Scholar 

  15. Nordmann, A., Hochgeschwender, N., Wigand, D., Wrede, S.: A survey on domain-specific modeling and languages in Robotics. J. Softw. Eng. Robot. 7(1), 75–99 (2016)

    Google Scholar 

  16. Foughali, M., Berthomieu, B., Dal Zilio, S., Ingrand, F., Mallet, A.: Model checking real-time properties on the functional layer of autonomous robots. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 383–399. Springer, Cham (2016). doi:10.1007/978-3-319-47846-3_24

    Chapter  Google Scholar 

  17. Fleurey, F., Solberg, A.: A domain specific modeling language supporting specification, simulation and execution of dynamic adaptive systems. In: Schürr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 606–621. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04425-0_47

    Chapter  Google Scholar 

  18. Musliner, D.J., Durfee, E.H., Shin, K.G.: CIRCA: a cooperative intelligent real-time control architecture. IEEE Trans. Syst. Man Cybern. 23(6), 1561–1574 (1993)

    Article  Google Scholar 

  19. Espiau, B., Kapellos, K., Jourdan, M.: Formal verification in robotics: why and how? In: Giralt, G., Hirzinger, G. (eds.) Robotics Research, pp. 225–236. Springer, London (1996)

    Chapter  Google Scholar 

  20. Schlegel, C., Hassler, T., Lotz, A., Steck, A.: Robotic software systems: from code-driven to model-driven designs. In: International Conference on Advanced Robotics, ICAR 2009, 1–8 June 2009

    Google Scholar 

  21. Dhouib, S., Kchir, S., Stinckwich, S., Ziadi, T., Ziane, M.: RobotML, a domain-specific language to design, simulate and deploy robotic applications. In: Noda, I., Ando, N., Brugali, D., Kuffner, J.J. (eds.) SIMPAR 2012. LNCS (LNAI), vol. 7628, pp. 149–160. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34327-8_16

    Chapter  Google Scholar 

  22. Rasch, H., Wehrheim, H.: Checking consistency in UML diagrams: classes and state machines. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 229–243. Springer, Heidelberg (2003). doi:10.1007/978-3-540-39958-2_16

    Chapter  Google Scholar 

  23. Davies, J., Crichton, C.: Concurrency and refinement in the unified modeling language. Formal Aspects Comput. 15(2–3), 118–145 (2003)

    Article  MATH  Google Scholar 

  24. Selic, B., Grard, S.: Modeling and Analysis of Real-Time and Embedded Systems with UML and MARTE: Developing Cyber-Physical Systems. Morgan Kaufmann Publishers Inc., Burlington (2013)

    Google Scholar 

  25. Selic, B.: Using UML for modeling complex real-time systems. In: Mueller, F., Bestavros, A. (eds.) LCTES 1998. LNCS, vol. 1474, pp. 250–260. Springer, Heidelberg (1998). doi:10.1007/BFb0057795

    Chapter  Google Scholar 

  26. Ramos, R., Sampaio, A., Mota, A.: A semantics for UML-RT active classes via mapping into circus. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 99–114. Springer, Heidelberg (2005). doi:10.1007/11494881_7

    Chapter  Google Scholar 

  27. Akhlaki, K.B., Tunon, M.I.C., Terriza, J.A.H., Morales, L.E.M.: A methodological approach to the formal specification of real-time systems by transformation of UML-RT design models. Sci. Comput. Program. 65(1), 41–56 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  28. Zic, J.J.: Time-constrained buffer specifications in CSP + T and timed CSP. ACM Trans. Program. Lang. Syst. 16(6), 1661–1674 (1994)

    Article  Google Scholar 

  29. Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  30. Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL — a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996). doi:10.1007/BFb0020949

    Chapter  Google Scholar 

  31. Miyazawa, A., et al.: RoboChart reference manual. Technical report, University of York (2017). http://bit.ly/2plUry4

  32. RoboCalc Project: RoboChart Case Studies (2017).www.cs.york.ac.uk/circus/RoboCalc/case-studies/

Download references

Acknowledgments

This work is funded by EPSRC grant EP/M025756/1. No new primary data was created during this study.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, York, YO10 5GH, UK

    Pedro Ribeiro, Alvaro Miyazawa & Ana Cavalcanti

  2. Department of Electronic Engineering, University of York, York, YO10 5DD, UK

    Wei Li & Jon Timmis

Authors
  1. Pedro Ribeiro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alvaro Miyazawa
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wei Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ana Cavalcanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Jon Timmis
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pedro Ribeiro .

Editor information

Editors and Affiliations

  1. Massachusetts Institute of Technology, Cambridge, Massachusetts, USA

    Nadia Polikarpova

  2. University of Surrey, Guildford, United Kingdom

    Steve Schneider

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Ribeiro, P., Miyazawa, A., Li, W., Cavalcanti, A., Timmis, J. (2017). Modelling and Verification of Timed Robotic Controllers. In: Polikarpova, N., Schneider, S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science(), vol 10510. Springer, Cham. https://doi.org/10.1007/978-3-319-66845-1_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66845-1_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66844-4

  • Online ISBN: 978-3-319-66845-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation