Top

Journal of Combinatorial Optimization

Published in:

17-07-2018

Verifying schedulability of tasks in ROS-based systems

Authors: Jin Cui, Cong Tian, Nan Zhang, Zhenhua Duan, Hongwei Du

Published in: Journal of Combinatorial Optimization | Issue 3/2019

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Robot operating system (ROS) is a new programming framework for developing artificial intelligence systems, like robots, unmanned systems, etc. These systems are usually real-time systems. There are multi-tasks to be scheduled by the underlying real-time operating system. Ensuring schedulability of tasks in ROS-based systems (ROS systems for short) is essential for correctness and safety of such systems. This paper employs a model checking approach to verifying schedulability of tasks in ROS systems. In order to verify ROS systems, we investigate the operational semantics of TMSVL programs and develop an interpreter for it. As a case study, the scheduability of tasks in ROS systems is modeled in TMSVL and verified using its interpreter.

previous article Client assignment problems for latency minimization

next article A possible optimal design of one-way Hamming network H(n, 3) based on the minimum transmission latency

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Alur R (1999) Timed automata. In: International conference on computer aided verification. Springer, pp 8–22

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

Behrmann G, David A, Larsen KG (2004) A tutorial on uppaal. In: Formal methods for the design of real-time systems. Springer, Berlin, pp 200–236

Bel Mokadem H, Berard B, Gourcuff V, De Smet O, Roussel JM (2010) Verification of a timed multitask system with UPPAAL. IEEE Trans Autom Sci Eng 7(4):921–932CrossRef

Bini E, Buttazzo GC (2004) Schedulability analysis of periodic fixed priority systems. IEEE Trans Comput 53(11):1462–1473CrossRef

Bini E, Buttazzo GC, Buttazzo GM (2003) Rate monotonic analysis: the hyperbolic bound. IEEE Trans Comput 52(7):933–942CrossRef

Bucci G, Fedeli A, Sassoli L, Vicario E (2004) Timed state space analysis of real-time preemptive systems. IEEE Trans Softw Eng 30(2):97–111CrossRef

Cui J, Duan Z, Tian C, Du H, Zhang N (2018) A novel approach to modeling and verifying real-time systems for high reliability. IEEE Trans Reliab 67(2):481–493CrossRef

Cui J, Duan Z, Tian C, Zhang N (2018) Modeling and analysis of nested interrupt systems. J Softw 29(6):1670–1680 (in Chinese) MathSciNetMATH

Dennis L, Fisher M, Slavkovik M, Webster M (2016) Formal verification of ethical choices in autonomous systems. Robot Auton Syst 77:1–14CrossRef

Duan Z, Tian C (2014) A practical decision procedure for propositional projection temporal logic with infinite models. Theor Comput Sci 554:169–190MathSciNetCrossRefMATH

Duan Z, Tian C, Zhang N (2016) A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Theor Comput Sci 609:544–560MathSciNetCrossRefMATH

Katoen JS (2008) Principles of model checking. The MIT Press, CambridgeMATH

Kortenkamp D, Simmons R, Brugali D (2016) Robotic systems architectures and programming. In: Springer Handbook of Robotics. Springer, Berlin, pp 283–306

Labrosse JJ (2009) uC/OS-III, The real-time kernel. Micrium Press, Texas

Liu CL, Layland JW (1973) Scheduling algorithms for multiprogramming in a hard-real-time environment. JACM 20(1):46–61MathSciNetCrossRefMATH

Liu J, Zhou M, Song X, Gu M, Sun J (2017) Formal modeling and verification of a rate-monotonic scheduling implementation with real-time maude. IEEE Trans Ind Electron 64(4):3239–3249CrossRef

Mitsch S, Ghorbal K, Vogelbacher D, Platzer A (2017) Formal verification of obstacle avoidance and navigation of ground robots. Int J Robot Res 36(12):1312–1340CrossRef

Munoz CA, Dutle A, Narkawicz A, Upchurch J (2016) Unmanned aircraft systems in the national airspace system: a formal methods perspective. ACM SIGLOG News 3(3):67–76

Park J, Lee I, Sokolsky O, Hwang DY, Ahn S, Choi JY, Kang I (2017) A process algebraic approach to the schedulability analysis and workload abstraction of hierarchical real-time systems. J Log Algebraic Methods Program 92:1–18MathSciNetCrossRefMATH

Quigley M, Conley K, Gerkey B, Faust J, Foote T, Leibs J, Wheeler R, Ng AY (2009) ROS: an open-source robot operating system. In: ICRA workshop on open source software, vol 3. IEEE Press, p 5

Sun J, Liu Y, Dong JS, Liu Y, Shi L, André É (2013) Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans Softw Eng Methodol 22(1):3CrossRef

Sun J, Liu Y, Dong JS, Pang J (2009) PAT: towards flexible verification under fairness. In: CAV, vol 9. Springer, Berlin, pp 709–714

Wang M, Tian C, Duan Z (2017) Full regular temporal property verification as dynamic program execution. In: Proceedings of the 39th international conference on software engineering companion. IEEE Press, pp 226–228

Wang X, Tian C, Duan Z, Zhao L (2017) MSVL: a typed language for temporal logic programming. Front Comput Sci 11(5):762–785CrossRef

Waszniowski L, Hanzálek Z (2008) Formal verification of multitasking applications based on timed automata model. Real-Time Syst 38(1):39–65CrossRefMATH

Wei H, Shao Z, Huang Z, Chen R, Guan Y, Tan J, Shao Z (2016) RT-ROS: a real-time ROS architecture on multi-core processors. Future Gener Comput Syst 56:171–178CrossRef

Yang X, Duan Z (2008) Operational semantics of framed tempura. J Logic Algebraic Program 78(1):22–51MathSciNetCrossRefMATH

Zhang N, Duan Z, Tian C (2016) A mechanism of function calls in MSVL. Theor Comput Sci 654:11–25MathSciNetCrossRefMATH

Zhang N, Duan Z, Tian C (2016) Model checking concurrent systems with MSVL. Sci China Inf Sci 59(11):118101CrossRef

Title: Verifying schedulability of tasks in ROS-based systems
Authors: Jin Cui
Cong Tian
Nan Zhang
Zhenhua Duan
Hongwei Du
Publication date: 17-07-2018
Publisher: Springer US
Published in: Journal of Combinatorial Optimization / Issue 3/2019
Print ISSN: 1382-6905
Electronic ISSN: 1573-2886
DOI: https://doi.org/10.1007/s10878-018-0328-0

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 3/2019

A note on a two-agent scheduling problem related to the total weighted late work

A possible optimal design of one-way Hamming network H(n, 3) based on the minimum transmission latency

Competitive analysis of randomized online strategies for the multi-agent k-Canadian Traveler Problem

Operating room planning and surgical case scheduling: a review of literature

Approximation algorithms for the graph balancing problem with two speeds and two job lengths

Client assignment problems for latency minimization

Premium Partner