Abstract
Software is an essential part of robotic systems. As robots and autonomous systems are more and more deployed in human environments, we need to use elaborate validation and verification techniques in order to gain a higher level of trust in our systems. This motivates our determination to apply formal verification methods to robotics software. In this paper, we describe our results obtained using model-checking on the functional layer of an autonomous robot. We implement an automatic translation from GenoM, a robotics model-based software engineering framework, to the formal specification language Fiacre. This translation takes into account the semantics of the robotics middleware. TINA, our model-checking toolbox, can be used on the synthesized models to prove real-time properties of the functional modules implementation on the robot. We illustrate our approach using a realistic autonomous navigation example.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
- 3.
Codels (code elements) are the programmer implementation of the specified service, broken down to small chunks of C or C++ code.
- 4.
- 5.
- 6.
The template still provides the user with the possibility to specify their hardware constraints.
References
Abdeddaïm, Y., Asarin, E., Gallien, M., Ingrand, F., Lesire, C., Sighireanu, M.: Planning robust temporal plans: a comparison between CBTP and TGA approaches. In: ICAPS (2007)
Abdellatif, T., Bensalem, S., Combaz, J., de Silva, L., Ingrand, F.: Rigorous design of robot software: a formal component-based approach. Robot. Auton. Syst. 60, 1563–1578 (2012)
Abid, N., Dal Zilio, S., Le Botlan, D.: A formal framework to specify and verify real-time properties on critical systems. Int. J. Crit. Comput. Based Syst. 5(1), 4–30 (2014)
Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: SEFM, pp. 3–12 (2006)
Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-Finder: a tool for compositional deadlock detection and verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 614–619. Springer, Heidelberg (2009)
Berthomieu, B., Bodeveix, J.-P., Farail, P., Filali, M., Garavel, H., Gaufillet, P., Lang, F., Vernadat, F.: Fiacre: an intermediate language for model verification in the topcased environment. In: ERTS, HAL - CCSD, Toulouse (2008)
Berthomieu, B., Dal Zilio, S., Fronc, Ł.: Model-checking real-time properties of an aircraft landing gear system using fiacre. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 110–125. Springer, Heidelberg (2014)
Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. IFIP Congr. Ser. 9, 41–46 (1983)
Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA - construction of abstract state spaces for Petri nets and Time Petri. Int. J. Prod. Res. 42(14), 2741–2756 (2004)
Berthomieu, B., Vernadat, F.: State Space Abstractions for Time Petri Nets. Handbook of Real-Time and Embedded Systems. CRC Press, Boca Raton (2007)
Bourdil, P.-A., Berthomieu, B., Jenn, E.: Model-checking real-time properties of an auto flight control system function. In: IEEE ISSREW (2014)
Boussinot, F., de Simone, R.: The ESTEREL Language. In: Proceeding of the IEEE, pp. 1293–1304, September 1991
Brat, G., Denney, E., Giannakopoulou, D., Frank, J., Jónsson, A.K.: Verification of autonomous systems for space applications. In: IEEE Aerospace Conference (2006)
Brugali, D.: Model-driven software engineering in robotics. IEEE Robot. Autom. Mag. 22(3), 155–166 (2015)
Bruyninckx, H.: Open robot control software: the OROCOS project. In: IEEE International Conference on Robotics and Automation (2001)
Cimatti, A., Roveri, M., Bertoli, P.: Conformant planning via symbolic model checking and heuristic search. Artif. Intell. 159, 127–206 (2004)
Dolginova, E., Lynch, N.: Safety verification for automated platoon maneuvers: a case study. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 154–170. Springer, Heidelberg (1997)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE (1999)
Espiau, B., Kapellos, K., Jourdan, M.: Formal verification in robotics: why and how? In: Giralt, G., Hirzinge, G. (eds.) Robotics Research. Springer, London (1996)
Gobillot, N., Lesire, C., Doose, D.: A modeling framework for software architecture specification and validation. In: Brugali, D., Broenink, J.F., Kroeger, T., MacDonald, B.A. (eds.) SIMPAR 2014. LNCS, vol. 8810, pp. 303–314. Springer, Heidelberg (2014)
Hähnel, D., Burgard, W., Lakemeyer, G.: GOLEX—bridging the gap between logic (GOLOG) and a real robot. In: Herzog, O. (ed.) KI 1998. LNCS, vol. 1504, pp. 165–176. Springer, Heidelberg (1998)
Ingrand, F., Ghallab, M.: Deliberation for autonomous robots: a survey. Artif. Intell. 1–40 (2014). Elsevier
Ingrand, F., Lacroix, S., Lemai-Chenevier, S., Py, F.: Decisional autonomy of planetary rovers. J. Field Robot. 24(7), 559–580 (2007)
Mallet, A., Pasteur, C., Herrb, M., Lemaignan, S., Ingrand, F.: GenoM3: building middleware-independent robotic components. In: IEEE ICRA (2010)
Maraninchi, F.: Operational and compositional semantics of synchronous automaton compositions. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 550–564. Springer, Heidelberg (1992)
Merlin, P.M., Farber, D.J.: Recoverability of communication protocols: implications of a theoretical study. IEEE Trans. Commun. 24(9), 1036–1043 (1976)
Quigley, M., Gerkey, B., Conley, K., Faust, J., Foote, T., Leibs, J., Berger, E., Wheeler, R., Ng, A.Y.: ROS: an open-source Robot Operating System. In: IEEE ICRA (2009)
Rangra, S., Gaudin, E.: SDL to Fiacre translation. In: Embedded Real-Time Software and Systems, Toulouse (2014)
Simmons, R., Pecheur, C.: Automating model checking for autonomous systems. In: AAAI Spring Symposium on Real-Time Autonomous Systems (2000)
Simon, D., Joubert, A.: ORCCAD: towards an open robot controller computer aided design system. Technical report, Research report 1396, INRIA (1991)
Täubig, H.H., Frese, U., Hertzberg, C., Lüth, C., Mohr, S., Vorobev, E., Walter, D.: Guaranteeing functional safety: design for provability and computer-aided verification. Auton. Robots 32(3), 303–331 (2011)
Wongpiromsarn, T., Murray, R.M.: Formal verification of an autonomous vehicle system. In: Conference on Decision and Control, May 2008
Acknowledgement
This work was supported in part by the EU CPSE Labs project funded by the H2020 program under grant agreement No. 644400.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Foughali, M., Berthomieu, B., Dal Zilio, S., Ingrand, F., Mallet, A. (2016). 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. ICFEM 2016. Lecture Notes in Computer Science(), vol 10009. Springer, Cham. https://doi.org/10.1007/978-3-319-47846-3_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-47846-3_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47845-6
Online ISBN: 978-3-319-47846-3
eBook Packages: Computer ScienceComputer Science (R0)