1 - 3 of 3
rss atomLink til resultatlisten
Permanent link
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
  • html
  • text
  • asciidoc
  • rtf
  • Presentation: 2024-08-20 13:15 Kappa, Västerås
    Martin, Joyce
    Mälardalens universitet, Akademin för innovation, design och teknik, Inbyggda system.
    Towards Mission and Capability Modelling for Systems of Systems2024Licentiatavhandling, med artikler (Annet vitenskapelig)
  • Presentation: 2024-09-17 13:30 U2-024 och via Zoom, Västerås
    Dust, Lukas
    Mälardalens universitet, Akademin för innovation, design och teknik, Inbyggda system.
    Verifying ROS 2 Based Distributed Robotic Systems2024Licentiatavhandling, med artikler (Annet vitenskapelig)
    Abstract [en]

    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.

  • Presentation: 2024-10-03 09:15 Gamma, Västerås
    Mählkvist, Simon
    Mälardalens universitet, Akademin för ekonomi, samhälle och teknik. Kanthal AB, Sweden.
    Cost-Conscious Analytics and Decision Support for Industrial Batch Processes2024Licentiatavhandling, med artikler (Annet vitenskapelig)