Skip to main content

Sound Simulation and Co-simulation for Robotics

  • Chapter
  • First Online:

Abstract

Software engineering for modern robot applications needs attention; current practice suffers from costly iterations of trial and error, with hardware and environment in the loop. We propose the adoption of an approach to simulation and co-simulation of robotics applications where designs and (co-)simulations are amenable to verification. In this approach, designs are composed of several (co-)models whose relationship is defined using a SysML profile. Simulation is the favoured technique for analysis in industry, and co-simulation enables the orchestrated use of a variety of simulation tools, including, for instance, reactive simulators and simulators of control laws. Here, we define the SysML profile that we propose and give it a process algebraic semantics. With that semantics, we capture the properties of the SysML model that must be satisfied by a co-simulation. Our long-term goal is to support validation and verification beyond what can be achieved with simulation.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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  Google Scholar 

  2. Amálio, N.: Foundations of the SysML profile for CPS modelling. Technical Report D2.1a, INTO-CPS project (2015)

    Google Scholar 

  3. Bastian, J., Clauß, C., Wolf, S., Schneider, P.: Master for co-simulation using FMI. In: Modelica Conference (2011)

    Book  Google Scholar 

  4. Broenink, J.F.: Modelling, simulation and analysis with 20-sim. Comput. Aided Control Syst. Des. 38(3), 22–25 (1997)

    Google Scholar 

  5. Broman, D., Brooks, C., Greenberg, L., Lee, E.A., Masin, M., Tripakis, S., Wetter, M.: Determinate composition of FMUs for co-simulation. In: ACM SIGBED International Conference on Embedded Software. IEEE, New York (2013)

    Book  Google Scholar 

  6. Broy, M., Cengarle, M.V., Rumpe, B.: Semantics of UML – towards a system model for UML: the state machine model. Technical Report TUM-I0711, Institut für Informatik, Technische Universität München (2007)

    Google Scholar 

  7. Bubeck, A., Weisshardt, F., Sing, T., Reiser, U., Hagele, M., Verl, A.: Implementing best practices for systems integration and distributed software development in service robotics-the care-o-bot®; robot family. In: 2012 IEEE/SICE International Symposium on System Integration, pp. 609–614. IEEE, New York (2012)

    Google Scholar 

  8. Cavalcanti, A.L.C., Clayton, P., O’Halloran, C.: From control law diagrams to ada via Circus. Form. Asp. Comput. 23(4), 465–512 (2011)

    Article  Google Scholar 

  9. Cavalcanti, A.L.C., Woodcock, J.C.P., Amálio, N.: Behavioural models for FMI Co-simulations. Technical Report, University of York, Department of Computer Science, York (2016). Available at www-users.cs.york.ac.uk/~alcc/CWA16.pdf

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  11. Denil, J., Meyers, B., De Meulenaere, P., Vangheluwe, H.: Explicit semantic adaptation of hybrid formalisms for FMI co-simulation. In: Spring Simulation Multi-Conference (2015)

    Google Scholar 

  12. Dhouib, S., Kchir, S., Stinckwich, S., Ziadi, T., Ziane, M.: RobotML, a domain-specific language to design, simulate and deploy robotic applications. In: Simulation, Modeling, and Programming for Autonomous Robots, pp. 149–160. Springer, Berlin (2012)

    Chapter  Google Scholar 

  13. Eshuis, R.: Reconciling statechart semantics. Sci. Comput. Program. 74(3), 65–99 (2009)

    Article  MathSciNet  Google Scholar 

  14. Feldman, Y.A., Greenberg, L., Palachi, E.: Simulating rhapsody SysML blocks in hybrid models with FMI. In: Modelica Conference (2014)

    Book  Google Scholar 

  15. FMI development group. Functional mock-up interface for model exchange and co-simulation, 2.0 (2014). https://www.fmi-standard.org

  16. Foster, S., Zeyda, F., Woodcock, J.C.P.: Isabelle/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) Unifying Theories of Programming. Lecture Notes in Computer Science, vol. 8963, pp. 21–41. Springer, Berlin (2015)

    Google Scholar 

  17. 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.) Formal Methods and Software Engineering, pp. 383–399. Springer, Berlin (2016)

    Chapter  Google Scholar 

  18. Fritzson, P.: Principles of Object-Oriented Modeling and Simulation with Modelica 2.1. Wiley-IEEE, New York (2004)

    Book  Google Scholar 

  19. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 187–201 (2014)

    Chapter  Google Scholar 

  20. Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)

    Article  MathSciNet  Google Scholar 

  21. 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. Part C Appl. Rev. 42(6), 1730–1741 (2012)

    Article  Google Scholar 

  22. Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs, NJ (1998)

    MATH  Google Scholar 

  23. Klein, J., Spector, L.: 3D Multi-agent simulations in the breve simulation environment. In: Artificial Life Models in Software, pp. 79–106. Springer, Berlin (2009)

    Chapter  Google Scholar 

  24. Kuske, S., Gogolla, M., Kollmann, R., Kreowski, H.-J.: An integrated semantics for UML class, object and state diagrams based on graph transformation. In: Butler, M., Petre, L., SereKaisa, K. (eds.) Integrated Formal Methods. Lecture Notes in Computer Science, vol. 2335, pp. 11–28. Springer, Berlin (2002)

    Chapter  Google Scholar 

  25. Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The overture initiative – integrating tools for VDM. SIGSOFT Softw. Eng. Notes 35(1), 1–6 (2010)

    Article  Google Scholar 

  26. Luke, S., Cioffi-Revilla, C., Panait, L., Sullivan, K., Balan, G.: Mason: a multiagent simulation environment. Simulation 81(7), 517–527 (2005)

    Article  Google Scholar 

  27. Mallet, A., Pasteur, C., Herrb, M., Lemaignan, S., Ingrand, F.: Genom3: building middleware-independent robotic components. In: 2010 IEEE International Conference on Robotics and Automation, pp. 4627–4632 (2010)

    Google Scholar 

  28. Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A.L.C., Timmis, J., Woodcock, J.C.P.: RoboChart: a state-machine notation for modelling and verification of mobile and autonomous robots. Technical Report, University of York, Department of Computer Science, York (2016). Available at www.cs.york.ac.uk/circus/publications/techreports/reports/MRLCTW16.pdf

    Google Scholar 

  29. Object Management Group: OMG Unified Modeling Language (OMG UML), Superstructure, Version 2.4.1 (2011)

    Google Scholar 

  30. OMG: OMG Systems Modeling Language (OMG SysML), Version 1.3 (2012)

    Google Scholar 

  31. Pohlmann, U., Schäfer, W., Reddehase, H., Röckemann, J., Wagner, R.: Generating functional mockup units from software specifications. In: Modelica Conference (2012)

    Book  Google Scholar 

  32. Ramos, R., Sampaio, A.C.A., Mota, A.C.: A semantics for UML-RT active classes via mapping into Circus. In: Formal Methods for Open Object-based Distributed Systems. Lecture Notes in Computer Science, vol. 3535, pp. 99–114 (2005)

    Google Scholar 

  33. Rasch, H., Wehrheim, H.: Checking consistency in UML diagrams: classes and state machines. In: Najm, E., Nestmann, U., Stevens, P. (eds.) Formal Methods for Open Object-Based Distributed Systems. Lecture Notes in Computer Science, vol. 2884, pp. 229–243. Springer, Berlin (2003)

    Chapter  Google Scholar 

  34. Rohmer, E., Singh, S.P.N., Freese, M.: V-rep: a versatile and scalable robot simulation framework. In: IEEE International Conference on Intelligent Robots and Systems, vol. 1, pp. 1321–1326. IEEE, New York (2013)

    Google Scholar 

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

    MATH  Google Scholar 

  36. Savicks, V., Butler, M., Colley, J.: Co-simulating event-B and continuous models via FMI. In: Summer Simulation Multiconference, pp. 37:1–37:8. Society for Computer Simulation International, San Diego (2014)

    Google Scholar 

  37. Savicks, V., Butler, M., Colley, J.: Co-simulation environment for Rodin: landing gear case study. In: Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K.-D. (eds.) International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 148–153. Springer, Berlin (2014)

    Google Scholar 

  38. Schlegel, C., Hassler, T., Lotz, A., Steck, A.: Robotic software systems: from code-driven to model-driven designs. In: 14th International Conference on Advanced Robotics, pp. 1–8. IEEE, New York (2009)

    Google Scholar 

  39. Schneider, S.: Concurrent and Real-time Systems: The CSP Approach. Wiley, New York (2000)

    Google Scholar 

  40. Schultz, U.P., Johan, C.D., Stoy, K.: A domain-specific language for programming self-reconfigurable robots. In: Workshop on Automatic Program Generation for Embedded Systems (APGES), pp. 28–36 (2007)

    Google Scholar 

  41. Selic, B.: Using UML for modeling complex real-time systems. In: Mueller, F., Bestavros, A. (eds.) Languages, Compilers, and Tools for Embedded Systems. Lecture Notes in Computer Science, vol. 1474, pp. 250–260. Springer, Berlin (1998)

    Chapter  Google Scholar 

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

    Google Scholar 

  43. The MathWorks, Inc.: Simulink. www.mathworks.com/products/simulink

  44. Tripakis, S.: Bridging the semantic gap between heterogeneous modeling formalisms and FMI. In: International Conference on Embedded Computer Systems: Architectures, Modeling, and Simulation, pp. 60–69. IEEE, New York (2015)

    Google Scholar 

  45. Woodcock, J.C.P., Cavalcanti, A.L.C.: Circus: a concurrent refinement language. Technical Report, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford (2001)

    Google Scholar 

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

    Article  Google Scholar 

Download references

Acknowledgements

This work is funded by the INTO-CPS EU grant and EPSRC grant EP/M025756/1. The authors are grateful to Wei Li, Pedro Ribeiro, Augusto Sampaio, and Jon Timmis for many discussions on RoboChart and simulation of robotic applications. No new primary data was created during this study.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Ana Cavalcanti .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Cavalcanti, A., Miyazawa, A., Payne, R., Woodcock, J. (2017). Sound Simulation and Co-simulation for Robotics. In: Mazzara, M., Meyer, B. (eds) Present and Ulterior Software Engineering. Springer, Cham. https://doi.org/10.1007/978-3-319-67425-4_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67425-4_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67424-7

  • Online ISBN: 978-3-319-67425-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics