Skip to main content
SpringerLink
Log in

On Reconciling Schedulability Analysis and Model Checking in Robotics

  • Conference paper
  • First Online:
New Trends in Model and Data Engineering (MEDI 2019)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 1085))

Included in the following conference series:

Abstract

The challenges of deploying robots and autonomous vehicles call for further efforts to bring the real-time systems and the formal methods communities together. In this paper, we discuss the practicality of paramount model checking formalisms in implementing dynamic-priority-based cooperative schedulers, where capturing the waiting time of tasks has a major impact on scalability. Subsequently, we propose a novel technique that alleviates such an impact, and thus enables schedulability analysis and verification of real-time/behavioral properties within the same model checking framework, while taking into account hardware and OS specificities. The technique is implemented in an automatic translation from a robotic framework to UPPAAL, and evaluated on a real robotic example.

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. Robotnik Summit-XL data sheet. https://www.robotnik.eu/web/wp-content/uploads//2019/03/Robotnik_DATASHEET_SUMMIT-XL-HL_EN-web-1.pdf

  2. Alur, R.: Timed automata. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_3

    Chapter  Google Scholar 

  3. Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  5. Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES: a tool for schedulability analysis and code generation of real-time systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 60–72. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-40903-8_6

    Chapter  MATH  Google Scholar 

  6. André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_6

    Chapter  Google Scholar 

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

  8. Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA-construction of abstract state spaces for Petri nets and time Petri nets. J. Prod. Res. 42(14), 2741–2756 (2004)

    Article  Google Scholar 

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

  10. Díaz, J., et al.: Stochastic analysis of periodic real-time systems. In: RTSS, pp. 289–300. IEEE (2002)

    Google Scholar 

  11. Foughali, M.: Toward a correct-and-scalable verification of concurrent robotic systems: insights on formalisms and tools. In: ACSD, pp. 29–38 (2017)

    Google Scholar 

  12. 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: FormaliSE, pp. 2–9 (2018)

    Google Scholar 

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

  14. Foughali, M., Dal Zilio, S., Ingrand, F.: On the Semantics of the GenoM3 Framework. Technical report (2019)

    Google Scholar 

  15. Foughali, M., Ingrand, F., Seceleanu, C.: Statistical model checking of complex robotic systems. In: SPIN (2019)

    Google Scholar 

  16. Gobillot, N., Guet, F., Doose, D., Grand, C., Lesire, C., Santinelli, L.: Measurement-based real-time analysis of robotic software architectures. In: IROS, pp. 3306–3311. IEEE (2016)

    Google Scholar 

  17. Goddard, S., Huang, J., Farritor, S., et al.: A performance and schedulability analysis of an autonomous mobile robot. In: ECRTS, pp. 239–248. IEEE (2005)

    Google Scholar 

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

  19. Huang, X., Singh, A., Smolka, S.: Using integer clocks to verify clock-synchronization protocols. Innov. Syst. Softw. Eng. 7(2), 119–130 (2011)

    Article  Google Scholar 

  20. Kargahi, M., Movaghar, A.: Non-preemptive earliest-deadline-first scheduling policy: a performance study. In: MASCOTS, pp. 201–208. IEEE (2005)

    Google Scholar 

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

  22. Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54–57. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_6

    Chapter  Google Scholar 

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

    Google Scholar 

  24. Merlin, P., Farber, D.: Recoverability of Communication Protocols: Implications of a Theoretical Study. IEEE Transactions on Communications 24(9), 1036–1043 (1976)

    Article  MathSciNet  Google Scholar 

  25. Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J.: Automatic property checking of robotic applications. In: IROS, pp. 3869–3876. IEEE (2017)

    Google Scholar 

  26. Piaggio, M., Sgorbissa, A., Zaccaria, R.: Pre-emptive versus non-pre-emptive real time scheduling in intelligent mobile robotics. J. Exp. Theor. Artif. Intell. 12(2), 235–245 (2000)

    Article  Google Scholar 

  27. Sensfelder, N., Brunel, J., Pagetti, C.: Modeling cache coherence to expose interference. In: ECRTS (2019)

    Google Scholar 

  28. Shi, J., Goddard, S., Lal, A., Farritor, S.: A real-time model for the robotic highway safety marker system. In: RTAS, pp. 331–340. IEEE (2004)

    Google Scholar 

  29. Shih, C., Sha, L., Liu, J.: Scheduling tasks with variable deadlines. In: RTAS, pp. 120–122. IEEE (2001)

    Google Scholar 

  30. Sowmya, A., Tsz-Wang So, D., Hung Tang, W.: Design of a mobile robot controller using Esterel tools. Electron. Not. Theor. Comput. Sci. 65(5), 3–10 (2002)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Mohammed Foughali

Authors
  1. Mohammed Foughali
    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. University of Nantes, Nantes, France

    Christian Attiogbé

  2. Software Competence Center Hagenberg, Hagenberg, Austria

    Flavio Ferrarotti

  3. University of Bordeaux, Bordeaux, France

    Sofian Maabout

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. (2019). On Reconciling Schedulability Analysis and Model Checking in Robotics. In: Attiogbé, C., Ferrarotti, F., Maabout, S. (eds) New Trends in Model and Data Engineering. MEDI 2019. Communications in Computer and Information Science, vol 1085. Springer, Cham. https://doi.org/10.1007/978-3-030-32213-7_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32213-7_3

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation