Bachelor and Master Theses

To apply for conducting this thesis, please contact the thesis supervisor(s).
Title: Modeling and Analyzing Collaborating Heavy Machines
Subject: Computer science, Software engineering
Level: Advanced
Description: Target:
Modeling and analyzing collaborating autonomous machines, using different modeling languages and tool with different goals and analysis support, namely Rebeca, Ptolemy.



Motivation:
To build dependable systems we need to be able to have different techniques for thorough analysis. There is a wide range of analysis techniques, including testing, simulation, assertion check, light weight formal verification and statistical model checking. Building different models of the system, in various levels of abstraction, helps in managing the complexity in analyzing cyber physical systems and systems of systems. Different models and techniques are available with different features and supporting tools. Here we choose two platforms, Rebeca and Ptolemy, which both target distributed and concurrent systems, and can model timing constraints. Rebeca tools can check assertions and deadline misses, while Ptolemy shows the architecture and is supported by a powerful and visual simulation tool. Both tools provide performance evaluation and make it possible to explore the design space to make better design decisions.


Tasks:
• Reverse modeling from implementation in ROS towards Rebeca (and in a second project towards Ptolemy)
• Model-driven development by building the Rebeca model (or the Ptolemy model) and then map it to ROS
• Modeling [communication] collaboration protocols and behavior of collaborating Heavy Machines - Check the communication on different layers (hint: this can be a different project)

Sub-tasks:
• Learn Rebeca (Ptolemy) and its supporting tools
• Reverse-model the code: Map the [ROS] case study code to Rebeca (or Ptolemy)
• Model-driven development: Build the Rebeca model (or Ptolemy model) for a robot and then map it to ROS
• Automate the mapping between ROS and Rebeca (Ptolemy) (Note: we have preliminary results for the mapping from Rebeca to ROS and back as the outcome of two master theses.)
• Specify the safety and progress properties to check, like the minimum distance between machines, relation between the speed of a machine and its distance from others, no deadlock
• Specify the performance measurements, like maximum throughput of several collaborating machines, least waiting time for a service request to be completed
• Do the analysis: assertion-check and performance evaluation
• Model the architecture and check the design space, where to put what component


Expected Results:
• Algorithms for Mapping from ROS to Rebeca (or to Ptolemy)
• Algorithms for Mapping from Rebeca (or Ptolemy) to ROS
• Assertion check results
• Performance evaluation results
• Test cases
• Finding the bugs
• In case of Ptolemy – we get a simulation environment

Supervisor(s): Marjan Sirjani (marjan.sirjani@mdh.se)
Examiner:
Start date:
End date:
Prerequisites: Background on the following:
ROS: http://www.ros.org/
Rebeca: http://www.rebeca-lang.org/wiki/pmwiki.php
Ptolemy: http://ptolemy.eecs.berkeley.edu/
Drona: https://drona-org.github.io/Drona/
IDT supervisors:
Examiner:
Comments:
Company contact: Volvo CE Stephan Baumgart, Mail: stephan.baumgart@volvo.com, Phone: +46 16 541 8774