Verifying schedulability of tasks in ROS-based systems

Jin Cui (), Cong Tian (), Nan Zhang (), Zhenhua Duan () and Hongwei Du ()
Additional contact information
Jin Cui: Xidian University
Cong Tian: Xidian University
Nan Zhang: Xidian University
Zhenhua Duan: Xidian University
Hongwei Du: Harbin Institute of Technology

Journal of Combinatorial Optimization, 2019, vol. 37, issue 3, No 7, 920 pages

Abstract: 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.

Keywords: Formal verification; Schedulability; TMSVL; Operational semantics; Interpreter; Robot operating systems (search for similar items in EconPapers)
Date: 2019
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
http://link.springer.com/10.1007/s10878-018-0328-0 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:jcomop:v:37:y:2019:i:3:d:10.1007_s10878-018-0328-0

Ordering information: This journal article can be ordered from
https://www.springer.com/journal/10878

DOI: 10.1007/s10878-018-0328-0

Access Statistics for this article

Journal of Combinatorial Optimization is currently edited by Thai, My T.

More articles in Journal of Combinatorial Optimization from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().