Sökning: AMNE:(ENGINEERING AND TECHNOLOGY) AMNE:(Electrical Engineering Electronic Engineering Information Engineering) AMNE:(Robotics) >
Verifying ROS 2 Bas...
-
Dust, LukasMälardalens universitet,Inbyggda system
(författare)
Verifying ROS 2 Based Distributed Robotic Systems
Förlag, utgivningsår, omfång ...
-
Västerås :Mälardalens universitet,2024
-
printrdacarrier
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:mdh-67510
-
ISBN:9789174856705
-
https://urn.kb.se/resolve?urn=urn:nbn:se:mdh:diva-67510URI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:vet swepub-contenttype
-
Ämneskategori:lic swepub-publicationtype
Serie
-
Mälardalen University Press Licentiate Theses,1651-9256 ;363
Anmärkningar
-
Due to safety criticality, distributed robotic systems, such as Robot Operating System 2 (ROS 2) based applications, often have strict timing requirements. In this thesis, we attempt to simplify formal verification of the timing behaviour of ROS 2 based applications. Therefore, (i) we conduct experiments to determine and define patterns and semantics of ROS 2 task scheduling and execution, (ii) we propose a pattern-based formal approach of modeling and verifying ROS 2 applications via model checking in UPPAAL, and (iii) we propose a methodology for model-based development and verification of ROS 2 application designs. The thesis starts with a comprehensive evaluation of timing behavior, including the internal scheduling of ROS 2 applications, to define evaluation metrics and timing correctness. Based on the evaluation, buffer overflow and callback latency are defined as measures for timing errors. Furthermore, we identify application design patterns and parameters that can influence potential timing errors. To introduce and facilitate the use of formal methods, we propose pattern-based verification, using UPPAAL, creating reusable templates of important ROS 2 application components. Furthermore, we show how to apply the templates to model ROS 2 applications and verify potential buffer overflow and callback latencies. Finally, we propose a novel methodology for automation of verification in the context of ROS 2 that uses generated tracing information of ROS 2 executions to build structural models as class diagrams and, ultimately, formal models in the form of networks of UPPAAL timed automata for model checking. In our approach, one can apply the methodology as a framework that includes model checking as a back-end and, therefore, helping designers to bridge the gap between the ROS 2 code and formal analysis.
Ämnesord och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Ekström, Mikael
(preses)
-
Seceleanu, Cristina
(preses)
-
Mubeen, Saad
(preses)
-
Gu, Rong
(preses)
-
Tumova, Jana,Associate ProfessorKTH Royal Institute of Technology, Sweden
(opponent)
-
Mälardalens universitetInbyggda system
(creator_code:org_t)
Internetlänk
Hitta via bibliotek
Till lärosätets databas