Sound Simulation and Co-simulation for Robotics

  • Ana Cavalcanti
  • Alvaro Miyazawa
  • Richard Payne
  • Jim Woodcock


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.



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.


  1. 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)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Amálio, N.: Foundations of the SysML profile for CPS modelling. Technical Report D2.1a, INTO-CPS project (2015)Google Scholar
  3. 3.
    Bastian, J., Clauß, C., Wolf, S., Schneider, P.: Master for co-simulation using FMI. In: Modelica Conference (2011)CrossRefGoogle Scholar
  4. 4.
    Broenink, J.F.: Modelling, simulation and analysis with 20-sim. Comput. Aided Control Syst. Des. 38(3), 22–25 (1997)Google Scholar
  5. 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)CrossRefGoogle Scholar
  6. 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. 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. 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)CrossRefGoogle Scholar
  9. 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 CrossRefGoogle Scholar
  10. 10.
    Davies, J., Crichton, C.: Concurrency and refinement in the unified modeling language. Form. Asp. Comput. 15(2–3), 118–145 (2003)CrossRefGoogle Scholar
  11. 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. 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)CrossRefGoogle Scholar
  13. 13.
    Eshuis, R.: Reconciling statechart semantics. Sci. Comput. Program. 74(3), 65–99 (2009)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Feldman, Y.A., Greenberg, L., Palachi, E.: Simulating rhapsody SysML blocks in hybrid models with FMI. In: Modelica Conference (2014)CrossRefGoogle Scholar
  15. 15.
    FMI development group. Functional mock-up interface for model exchange and co-simulation, 2.0 (2014).
  16. 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. 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)CrossRefGoogle Scholar
  18. 18.
    Fritzson, P.: Principles of Object-Oriented Modeling and Simulation with Modelica 2.1. Wiley-IEEE, New York (2004)CrossRefGoogle Scholar
  19. 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)CrossRefGoogle Scholar
  20. 20.
    Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)MathSciNetCrossRefGoogle Scholar
  21. 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)CrossRefGoogle Scholar
  22. 22.
    Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs, NJ (1998)zbMATHGoogle Scholar
  23. 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)CrossRefGoogle Scholar
  24. 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)CrossRefGoogle Scholar
  25. 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)CrossRefGoogle Scholar
  26. 26.
    Luke, S., Cioffi-Revilla, C., Panait, L., Sullivan, K., Balan, G.: Mason: a multiagent simulation environment. Simulation 81(7), 517–527 (2005)CrossRefGoogle Scholar
  27. 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. 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 Google Scholar
  29. 29.
    Object Management Group: OMG Unified Modeling Language (OMG UML), Superstructure, Version 2.4.1 (2011)Google Scholar
  30. 30.
    OMG: OMG Systems Modeling Language (OMG SysML), Version 1.3 (2012)Google Scholar
  31. 31.
    Pohlmann, U., Schäfer, W., Reddehase, H., Röckemann, J., Wagner, R.: Generating functional mockup units from software specifications. In: Modelica Conference (2012)CrossRefGoogle Scholar
  32. 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. 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)CrossRefGoogle Scholar
  34. 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. 35.
    Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, Berlin (2011)zbMATHGoogle Scholar
  36. 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. 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. 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. 39.
    Schneider, S.: Concurrent and Real-time Systems: The CSP Approach. Wiley, New York (2000)Google Scholar
  40. 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. 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)CrossRefGoogle Scholar
  42. 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. 43.
    The MathWorks, Inc.: Simulink.
  44. 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. 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. 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)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Ana Cavalcanti
    • 1
  • Alvaro Miyazawa
    • 1
  • Richard Payne
    • 2
    • 3
  • Jim Woodcock
    • 1
  1. 1.Department of Computer ScienceUniversity of YorkYorkUK
  2. 2.School of Computing ScienceNewcastle UniversityNewcastle upon TyneUK
  3. 3.The Nine Software Company LimitedSouth TynesideUK

Personalised recommendations