Skip to main content
SpringerLink
Log in

Statistical Model Checking of Complex Robotic Systems

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11636))

Included in the following conference series:

Abstract

Failure of robotic software may cause catastrophic damages. In order to establish a higher level of trust in robotic systems, formal methods are often proposed. However, their applicability to the functional layer of robots remains limited because of the informal nature of specifications, their complexity and size. In this paper, we formalize the robotic framework and automatically translate its components to UPPAAL-SMC, a real-time statistical model checker. We apply our approach to verify properties of interest on a real-world autonomous drone navigation that does not scale with regular UPPAAL.

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

References

  1. The PocoLibs middleware. https://git.openrobots.org/projects/pocolibs

  2. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7

    Chapter  Google Scholar 

  3. Berry, G.: The Esterel v5 language primer: version v5\(\_\)91. Centre de mathématiques appliquées, Ecole des mines and INRIA (2000)

    Google Scholar 

  4. Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 103–129. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49213-5_5

    Chapter  Google Scholar 

  5. Bulychev, P., et al.: Monitor-based statistical model checking for weighted metric temporal logic. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 168–182. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28717-6_15

    Chapter  Google Scholar 

  6. Cappart, Q., Limbrée, C., Schaus, P., Quilbeuf, J., Traonouez, L.M., Legay, A.,Q.: Verification of interlocking systems using statistical model checking. In: 2017 IEEE 18th International Symposium on High Assurance Systems Engineering (HASE), pp. 61–68. IEEE (2017)

    Google Scholar 

  7. Cimatti, A., Roveri, M., Bertoli, P.: Conformant planning via symbolic model checking and heuristic search. Artif. Intell. 159(1–2), 127–206 (2004)

    Article  MathSciNet  Google Scholar 

  8. Foughali, M.: Toward a correct-and-scalable verification of concurrent robotic systems: insights on formalisms and tools. In: International Conference on Application of Concurrency to System Design (ACSD), pp. 29–38 (2017)

    Google Scholar 

  9. Foughali, M., Berthomieu, B., Dal Zilio, S., Hladik, P.E., Ingrand, F., Mallet, A.: Formal verification of complex robotic systems on resource-constrained platforms. In: International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 2–9 (2018)

    Google Scholar 

  10. 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). https://doi.org/10.1007/978-3-319-47846-3_24

    Chapter  Google Scholar 

  11. Foughali, M., Dal Zilio, S., Ingrand, F.: On the semantics of the GenoM3 framework. Technical report, LAAS-CNRS (2019)

    Google Scholar 

  12. Hähnel, D., Burgard, W., Lakemeyer, G.: GOLEX—Bridging the gap between logic (GOLOG) and a real robot. In: Herzog, O., Günter, A. (eds.) KI 1998. LNCS, vol. 1504, pp. 165–176. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0095437

    Chapter  Google Scholar 

  13. Halder, R., Proença, J., Macedo, N., Santos, A.: Formal verification of ROS-based robotic applications using timed-automata. In: International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 44–50. IEEE/ACM (2017)

    Google Scholar 

  14. Hazim, M.Y., Qu, H., Veres, S.M.: Testing, verification and improvements of timeliness in ROS processes. In: Alboul, L., Damian, D., Aitken, J.M.M. (eds.) TAROS 2016. LNCS (LNAI), vol. 9716, pp. 146–157. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40379-3_15

    Chapter  Google Scholar 

  15. Henzinger, T.A., Manna, Z., Pnueli, A.: Timed transition systems. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX 1991. LNCS, vol. 600, pp. 226–251. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0031995

    Chapter  Google Scholar 

  16. Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193–244 (1994)

    Article  MathSciNet  Google Scholar 

  17. Ingrand, F., Ghallab, M.: Deliberation for autonomous robots: a survey. Artif. Intell. 247, 10–44 (2017)

    Article  MathSciNet  Google Scholar 

  18. Kim, M., Kang, K.C.: Formal construction and verification of home service robots: a case study. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 429–443. Springer, Heidelberg (2005). https://doi.org/10.1007/11562948_32

    Chapter  Google Scholar 

  19. Kress-Gazit, H., Wongpiromsarn, T., Topcu, U.: Correct, reactive, high-level robot control. IEEE Robot. Autom. Mag. 18(3), 65–74 (2011)

    Article  Google Scholar 

  20. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  21. Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects Comput. 14, 295–318 (2003)

    Article  Google Scholar 

  22. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_11

    Chapter  Google Scholar 

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

    Google Scholar 

  24. Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J.: Automatic property checking of robotic applications. In: International Conference on Intelligent Robots and Systems (IROS), pp. 3869–3876. IEEE (2017)

    Google Scholar 

  25. Pecheur, C.: Verification and validation of autonomy software at NASA. Technical report, NASA Ames Research Center (2000)

    Google Scholar 

  26. Quigley, M., et al.: ROS: an open-source Robot Operating System. In: ICRA Workshop on Open Source Software, p. 5 (2009)

    Google Scholar 

  27. Roscoe, A.: Understanding Concurrent Systems. Springer, London (2010). https://doi.org/10.1007/978-1-84882-258-0

    Book  MATH  Google Scholar 

  28. Seceleanu, C., Vulgarakis, A., Pettersson, P.: REMES: a resource model for embedded systems. In: International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 84–94 (2009)

    Google Scholar 

  29. Sekizawa, T., Otsuki, F., Ito, K., Okano, K.: Behavior verification of autonomous robot vehicle in consideration of errors and sisturbances. In: International Computer Software and Applications Conference (COMPSAC), pp. 550–555 (2015)

    Google Scholar 

  30. Simon, D., Pissard-Gibollet, R., Arias, S.: Orccad, a framework for safe robot control design and implementation. In: National Workshop on Control Architectures of Robots: Software Approaches and Issues (CAR) (2006)

    Google Scholar 

  31. Sowmya, A., So, D.T.-W., Tang, W.H.: Design of a mobile robot controller using Esterel tools. Electron. Notes Theor. Comput. Sci. 65(5), 3–10 (2002)

    Article  Google Scholar 

  32. Tomatis, G., et al.: Designing a secure and robust mobile interacting robot for the long term. In: International Conference on Robotics and Automation (ICRA), pp. 4246–4251. IEEE (2003)

    Google Scholar 

  33. Volpe, R., Nesnas, I., Estlin, T., Mutz, D., Petras, R., Das, H.: The CLARAty architecture for robotic autonomy. In: Aerospace Conference, pp. 1–121 (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LAAS-CNRS, Université de Toulouse, CNRS, Toulouse, France

    Mohammed Foughali & Félix Ingrand

  2. Mälardalen University, Västerås, Sweden

    Cristina Seceleanu

Authors
  1. Mohammed Foughali
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Félix Ingrand
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Cristina Seceleanu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohammed Foughali .

Editor information

Editors and Affiliations

  1. Avast Software, Prague, Czech Republic

    Fabrizio Biondi

  2. Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Thomas Given-Wilson

  3. Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Axel Legay

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Foughali, M., Ingrand, F., Seceleanu, C. (2019). Statistical Model Checking of Complex Robotic Systems. In: Biondi, F., Given-Wilson, T., Legay, A. (eds) Model Checking Software. SPIN 2019. Lecture Notes in Computer Science(), vol 11636. Springer, Cham. https://doi.org/10.1007/978-3-030-30923-7_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30923-7_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30922-0

  • Online ISBN: 978-3-030-30923-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation