Abstract
This paper addresses the problem improving response times of robots implemented in the Robotic Operating System (ROS) using formal verification of computational-time feasibility. In order to verify the real time behaviour of a robot under uncertain signal processing times, methods of formal verification of timeliness properties are proposed for data flows in a ROS-based control system using Probabilistic Timed Programs (PTPs). To calculate the probability of success under certain time limits, and to demonstrate the strength of our approach, a case study is implemented for a robotic agent in terms of operational times verification using the PRISM model checker, which points to possible enhancements to the operation of the robotic agent.
This work was supported by the EPSRC project EP/J011894/2.
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
Aitken, J.M., Veres, S.M., Judge, M.: Adaptation of system configuration under the robot operating system. In: Proceedings of the 19th World Congress of the International Federation of Automatic Control (2014)
Dräger, K., Kwiatkowska, M.Z., Parker, D., Qu, H.: Local abstraction refinement for probabilistic timed programs. Theor. Comput. Sci. 538, 37–53 (2014)
Forouher, D., Hartmann, J., Maehle, E.: Data flow analysis in ROS. In: Proceedings of the 41st International Symposium on Robotics, pp. 1–6. VDE (2014)
Huang, J., Erdogan, C., Zhang, Y., Moore, B., Luo, Q., Sundaresan, A., Rosu, G.: ROSRV: runtime verification for robots. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 247–254. Springer, Heidelberg (2014)
Izzo, P., Qu, H., Veres, S.M.: Reducing complexity of autonomous control agents for verifiability. arXiv:1603.01202 [cs.SY], March 2016
Kwiatkowska, M., Norman, G., Parker, D.: A framework for verification of software with time and probabilities. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 25–45. Springer, Heidelberg (2010)
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)
Lincoln, N.K., Veres, S.M.: Natural language programming of complex robotic BDI agents. Intell. Robotic Syst. 71(2), 211–230 (2013)
Meng, W., Park, J., Sokolsky, O., Weirich, S., Lee, I.: Verified ROS-based deployment of platform-independent control systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 248–262. Springer, Heidelberg (2015)
Quigley, M., Conley, K., Gerkey, B.P., 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)
Webster, M., Dixon, C., Fisher, M., Salem, M., Saunders, J., Koay, K., Dautenhahn, K.: Formal verification of an autonomous personal robotic assistant, pp. 74–79. AAAI (2014)
Wooldridge, M.: An Introduction to MultiAgent Systems. Wiley, Chichester (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Hazim, M.Y., Qu, H., Veres, S.M. (2016). Testing, Verification and Improvements of Timeliness in ROS Processes. In: Alboul, L., Damian, D., Aitken, J. (eds) Towards Autonomous Robotic Systems. TAROS 2016. Lecture Notes in Computer Science(), vol 9716. Springer, Cham. https://doi.org/10.1007/978-3-319-40379-3_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-40379-3_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40378-6
Online ISBN: 978-3-319-40379-3
eBook Packages: Computer ScienceComputer Science (R0)