Thank you to those who joined the meeting. We had a good discussion and identified some concrete areas where we can take action. We also identified that our biggest roadblock is, as always, resources.
Here are my notes from the meeting.
Participants
- Alejandro Mosteo, author of the Ada client library. Working with drones, and don’t have a specific safety need but it is something that is of interest. Will continue maintaining the Ada client library and interested in SPARK.
- Brad Baillio, working on autonomous vehicles in off-road situations like mining and agriculture. Safety is an obvious need.
- Matt Droter, ROS Agriculture. Using ROS for farming so trying to figure out how to make it safe, what are the general best practices that can be applied.
- Nick Burek, AWS RoboMaker. Multiple groups at Amazon are doing robotics for warehouses, so the robots are safety-critical.
- Geoff Biggs, working on self-driving vehicles at Tier IV, where the importance of safety is obvious.
Discussion
- Client libraries:
- The Ada client library is working with Bouncy version of
rcl
, and feature complete for Bouncy. Alejandro is now going to update it to work with Dashingrcl
. - Alejandro plans to start working with SPARK in the near future.
- Rust is intriguing as a language that could be useful in safety, but it is not yet widely used in ROS. Working to classify Rust would be a huge job and probably beyond our capabilities.
- The Ada client library is working with Bouncy version of
- Tools in the work flow useful for safety-critical development with ROS.
- AWS work with TSAN and ASAN is now at the stage that reports are being generated in nightlies.
- The Automated Reasoning Group at Amazon uses a tool called C Bounded Model Checker (CBMC) that
allows you to write proofs against your code and allow you to check the whole valid range of inputs and outputs. It does C++ as well now, but is not great at multi-threaded logic. It is a good tool to find the last bugs in your code. - The same group is also using many other tools. Nick Burek will provide a list of tools being used.
- ROS QA WG is working on integrating the High Assurance ROS tool into the build farm.
- There is interest in the work that Apex.AI is doing. Are we duplicating their work, or are we trying to make their work open source? Are we competing?
- No one is particularly interested in and/or has the necessary skills to do formal specifications of nodes.
- Classifying tools used in ROS would be particularly valuable.
- We could try to classify launch2 or colcon. Both would be valuable for the community.
- We may be able to try and get Apex.AI on board for classifying launch, in particular its input specification.
- Most of the things discussed so far are tools that support reliability. What could we do to help people make sure their designs using ROS are safe?
- One particularly good idea is to come up with sample structures in ROS for common architecture patterns used in safety-critical systems, such as a 2oo3 architecture, or how a safety monitor should be implemented.
- Document how callback groups and how the threading models work with different executors so that people have a guide for how not to deadlock themselves, for example.
- Provide sample safety cases for ROS-based systems. ROS Agriculture has a small lawn tractor application, which is well-defined and has clear safety concerns. This could be a good sample application to work with. https://github.com/ros-agriculture/ros_lawn_tractor
Proposals
- Things to attempt:
- Document threading models used in ROS 2.
- Classify launch, especially its input specification, to find the things you should not do with it in a safety-critical system.
- Try CMBC and consider how it might be integrated into ament so it can be easily used in CI and the build farm.
- Develop some sample architectures for using ROS in a safety architecture, and document them.
- (Longer term) Produce a sample safety case for the ROS Agriculture small lawn tractor application.
- Possible effort contributions:
- Alejandro Mosteo can contribute some personal time, and if a student with interest comes along…
- Brad Baillio can contribute some personal time.
- Matt Droter can act as a conduit to the ROS QA WG to coordinate related efforts.
- Nick Burek will try and get some time on the next sprint at AWS for trying CMBC on at least one ROS package.
- Geoff Biggs can contribute work on sample architectures for safety-critical systems, will look into documenting the threading models, and over a longer term will work on the sample safety case with Matt.