SwePub
Sök i LIBRIS databas

  Utökad sökning

AMNE:(ENGINEERING AND TECHNOLOGY) AMNE:(Electrical Engineering Electronic Engineering Information Engineering) AMNE:(Robotics)
 

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

  • BokEngelska2024

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

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.

 
pil uppåt Stäng

Kopiera och spara länken för att återkomma till aktuell vy