|Title:||Modeling and Analyzing Collaborating Heavy Machines|
Modeling and analyzing collaborating autonomous machines, using different modeling languages and tool with different goals and analysis support, namely Rebeca, Ptolemy.
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.
Reverse modeling from implementation in ROS towards Rebeca (and in a second project towards Ptolemy)
Modeling [communication] collaboration protocols and behavior of collaborating Heavy Machines - Check the communication on different layers (hint: this can be a different project)
Learn Rebeca (Ptolemy) and its supporting tools
Reverse-model the code: Map the [ROS] case study code to Rebeca (Ptolemy)
Find the mapping between ROS and Rebeca (Ptolemy)
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
The Robot Operating System (ROS) is a flexible framework for writing robot software. It is a collection of tools, libraries, and conventions that aim to simplify the task of creating complex and robust robot behavior across a wide variety of robotic platforms.
Rebeca (Reactive Objects Language) is an actor-based language with a formal foundation, designed in an effort to bridge the gap between formal verification approaches and real applications. It can be considered as a reference model for concurrent computation, based on an operational interpretation of the actor model. It is also a platform for developing object-based concurrent systems in practice.
The Ptolemy project studies modeling, simulation, and design of concurrent, real-time, embedded systems. The focus is on assembly of concurrent components. The key underlying principle in the project is the use of well-defined models of computation that govern the interaction between components. A major problem area being addressed is the use of heterogeneous mixtures of models of computation.
Patterns from Mapping from ROS to Rebeca or to Ptolemy
Assertion check results
Performance evaluation results
Finding the bugs
In case of Ptolemy we get a simulation environment
|Company:||Volvo Construction Equipment, kontaktperson: Stephan Baumgart|