1 - 3 of 3
rss atomLink to result list
Permanent link
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
  • Presentation: 2024-08-20 13:15 Kappa, Västerås
    Martin, Joyce
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Towards Mission and Capability Modelling for Systems of Systems2024Licentiate thesis, comprehensive summary (Other academic)
  • Presentation: 2024-09-17 13:30 U2-024 och via Zoom, Västerås
    Dust, Lukas
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Verifying ROS 2 Based Distributed Robotic Systems2024Licentiate thesis, comprehensive summary (Other academic)
    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älardalen University, School of Business, Society and Engineering. Kanthal AB, Sweden.
    Cost-Conscious Analytics and Decision Support for Industrial Batch Processes2024Licentiate thesis, comprehensive summary (Other academic)