Verified ROS-Based Deployment of Platform-Independent Control Systems

  • Wenrui MengEmail author
  • Junkil Park
  • Oleg Sokolsky
  • Stephanie Weirich
  • Insup Lee
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)


The paper considers the problem of model-based deployment of platform-independent control code on a specific platform. The approach is based on automatic generation of platform-specific glue code from an architectural model of the system. We present a tool, ROSGen, that generates the glue code based on a declarative specification of platform interfaces. Our implementation targets the popular Robot Operating System (ROS) platform. We demonstrate that the code generation process is amenable to formal verification. The code generator is implemented in Coq and relies on the infrastructure provided by the CompCert and VST tool. We prove that the generated code always correctly connects the controller function to sensors and actuators in the robot. We use ROSGen to implement a cruise control system on the LandShark robot.


Global Variable Architectural Model Separation Logic Unmanned Ground Vehicle Controller Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Formal methods for the design of real-time systems, pp. 200–236. Springer (2004)Google Scholar
  2. 2.
    Halbwachs, N.: A synchronous language at work: the story of lustre. In: Formal Methods for Industrial Critical Systems: A Survey of Applications, pp. 15–31 (2005)Google Scholar
  3. 3.
    Quigley, M., Conley, K., Gerkey, B., Faust, J., Foote, T., Leibs, J., Wheeler, R., Ng, A.Y.: ROS: an open-source robot operating system. In: ICRA workshop on open source software, vol. 3 (2009)Google Scholar
  4. 4.
    The Coq development team: The Coq proof assistant reference manual. LogiCal Project, Version 8.0. (2004)Google Scholar
  5. 5.
    Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  6. 6.
    Meng, W., Park, J., Sokolsky, O., Weirich, S., Lee, I.: Verified ros-based deployment of platform-independent control systems. In: University of Pennsylvania Department of Computer and Information Science Technical Report No. MS-MS-CIS-15-01, February 2015Google Scholar
  7. 7.
    Leroy, X.: The compcert c verified compiler (2012)Google Scholar
  8. 8.
    Appel, A.W., Robert, D., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge University Press, UK (2014)CrossRefzbMATHGoogle Scholar
  9. 9.
    Pajic, M., Bezzo, N., Weimer, J., Sokolsky, O., Michael, N., Pappas, G.J., Tabuada, P., Lee, I.: Demo abstract: Synthesis of platform-aware attack-resilient vehicular systems. In: Cyber-Physical Systems (ICCPS), 2013 ACM/IEEE International Conference on, pp. 251–251. IEEE (2013)Google Scholar
  10. 10.
    Lasnier, G., Zalila, B., Pautet, L., Hugues, J.: Ocarina: an environment for AADL models analysis and automatic code generation for high integrity applications. In: Kordon, F., Kermarrec, Y. (eds.) Ada-Europe 2009. LNCS, vol. 5570, pp. 237–250. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  11. 11.
    Kim, B.G., Phan, L.T.X., Sokolsky, O., Lee, I.: Platform-dependent code generation for embedded real-time software. In: Compilers, Architecture and Synthesis for Embedded Systems (CASES), 2013 International Conference on, pp. 1–10. IEEE (2013)Google Scholar
  12. 12.
    Narayanan, A., Karsai, G.: Towards verifying model transformations. In: Proceedings of the 5\(^{th}\) International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2006), pp. 191–200 (2008)Google Scholar
  13. 13.
    Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. Journal of Systems and Software 83(2), 283–302 (2010)CrossRefGoogle Scholar
  14. 14.
    Lucio, L., Vangheluwe, H.: Model transformations to verify model transformations. In: Proceedings of the Workshop on Verification of Model Transformations, June 2013Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Wenrui Meng
    • 1
    Email author
  • Junkil Park
    • 1
  • Oleg Sokolsky
    • 1
  • Stephanie Weirich
    • 1
  • Insup Lee
    • 1
  1. 1.University of PennsylvaniaPhiladelphiaUSA

Personalised recommendations