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.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Robotnik Summit-XL data sheet. https://www.robotnik.eu/web/wp-content/uploads//2019/03/Robotnik_DATASHEET_SUMMIT-XL-HL_EN-web-1.pdf
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
Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)
Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
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
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
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
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)
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
Díaz, J., et al.: Stochastic analysis of periodic real-time systems. In: RTSS, pp. 289–300. IEEE (2002)
Foughali, M.: Toward a correct-and-scalable verification of concurrent robotic systems: insights on formalisms and tools. In: ACSD, pp. 29–38 (2017)
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)
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
Foughali, M., Dal Zilio, S., Ingrand, F.: On the Semantics of the GenoM3 Framework. Technical report (2019)
Foughali, M., Ingrand, F., Seceleanu, C.: Statistical model checking of complex robotic systems. In: SPIN (2019)
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)
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)
Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193–244 (1994)
Huang, X., Singh, A., Smolka, S.: Using integer clocks to verify clock-synchronization protocols. Innov. Syst. Softw. Eng. 7(2), 119–130 (2011)
Kargahi, M., Movaghar, A.: Non-preemptive earliest-deadline-first scheduling policy: a performance study. In: MASCOTS, pp. 201–208. IEEE (2005)
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
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
Mallet, A., Pasteur, C., Herrb, M., Lemaignan, S., Ingrand, F.: GenoM3: building middleware-independent robotic components. In: ICRA, pp. 4627–4632. IEEE (2010)
Merlin, P., Farber, D.: Recoverability of Communication Protocols: Implications of a Theoretical Study. IEEE Transactions on Communications 24(9), 1036–1043 (1976)
Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J.: Automatic property checking of robotic applications. In: IROS, pp. 3869–3876. IEEE (2017)
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)
Sensfelder, N., Brunel, J., Pagetti, C.: Modeling cache coherence to expose interference. In: ECRTS (2019)
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)
Shih, C., Sha, L., Liu, J.: Scheduling tasks with variable deadlines. In: RTAS, pp. 120–122. IEEE (2001)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
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)