Abstract
We consider the problem of automating the verification of distributed control software relying on publish-subscribe middleware. In this scenario, the main challenge is that software correctness depends intrinsically on correct usage of middleware components, but structured models of such components might not be available for analysis, e.g., because they are too large and complex to be described precisely in a cost-effective way. To overcome this problem, we propose to identify abstract models of middleware as finite-state automata, and then to perform verification on the combined middleware and control software models. Both steps are carried out in a computer-assisted way using state-of-the-art techniques in automata-based identification and verification. Our main contribution is to show that the combination of identification and verification is feasible and useful when considering typical issues that arise in the implementation of distributed control software.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aarts, F., Vaandrager, F.: Learning I/O automata. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 71–85. Springer, Heidelberg (2010)
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75(2), 87–106 (1987)
Baier, C., Katoen, J.: Principles of model checking. MIT Press, Cambridge (2008)
Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS) 8(2), 263 (1986)
De Alfaro, L., Henzinger, T.: Interface automata. ACM SIGSOFT Software Engineering Notes 26(5), 109–120 (2001)
Fitzpatrick, P., Metta, G., Natale, L.: Towards long-lived robot genes. Robotics and Autonomous Systems 56(1), 29–45 (2008)
Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. Logic Journal of IGPL 14(5), 729–744 (2006)
Holzmann, G.J.: The SPIN model checker: Primer and reference manual, vol. 1003. Addison-Wesley, Reading (2004)
Kearns, M., Vazirani, U.: An introduction to computational learning theory. MIT Press (1994)
Khalili, A., Tacchella, A.: Learning nondeterministic mealy machines. In: Proceedings of the 12th International Conference on Grammatical Inference (ICGI) ( to appear, 2014)
Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, pp. 137–151. ACM (1987)
Metta, G., Natale, L., Nori, F., Sandini, G., Vernon, D., Fadiga, L., von Hofsten, C., Rosander, K., Lopes, M., Santos-Victor, J., et al.: The iCub Humanoid Robot: An Open-Systems Platform for Research in Cognitive Development. Neural Networks: The Official Journal of the International Neural Network Society (2010)
Pratt, G., Manzo, J.: The DARPA Robotics Challenge [Competitions]. IEEE Robotics & Automation Magazine 20(2), 10–12 (2013)
Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
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)
Shahbaz, M.: Reverse Engineering Enhanced State Models of Black Box Software Components to Support Integration Testing. Ph.D. thesis, Institut Polytechnique de Grenoble, Grenoble, France (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Khalili, A., Natale, L., Tacchella, A. (2014). Reverse Engineering of Middleware for Verification of Robot Control Architectures. In: Brugali, D., Broenink, J.F., Kroeger, T., MacDonald, B.A. (eds) Simulation, Modeling, and Programming for Autonomous Robots. SIMPAR 2014. Lecture Notes in Computer Science(), vol 8810. Springer, Cham. https://doi.org/10.1007/978-3-319-11900-7_27
Download citation
DOI: https://doi.org/10.1007/978-3-319-11900-7_27
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11899-4
Online ISBN: 978-3-319-11900-7
eBook Packages: Computer ScienceComputer Science (R0)