Hi!
Not sure this is relevant to the original discussion -- I've just noticed "safety" and "protocols" in the name of the topic. At [our company](
https://www.imandra.ai/), we are working on tools and techniques for ensuring the safety and reliability of communication protocols by means of formal verification. So far we've been focusing on these types of problems in finance -- FinTech is essentially a distributed system of independent nodes communicating via messaging protocols. ROS looks like exactly the same kind of system, so we've also started a ROS-related project.
We are working on the creation of ROS-OCaml client -- if your code is written in a pure subset of OCaml, then it can be reasoned about using our Imandra proof assistant. Using Imandra, one can mathematically verify statements about your OCaml code, and it helps you to precisely formulate these formal statements by giving you counterexamples to your false claims. This allows you to create extremely reliable, precise and safe code and specification for it.
[1]: [Aesthetic Integration](
https://www.imandra.ai/)
[2]: [Try our Imandra reasoning engine in the browser](
https://try.imandra.ai/)
[3]: The GitHub of the project: [
https://github.com/AestheticIntegration/imandra-ros](
https://github.com/AestheticIntegration/imandra-ros)
---
[Visit Topic](
https://discourse.ros.org/t/using-safety-protocols-with-ros/5561/9) or reply to this email to respond.
If you do not want to receive messages from ros-users please use the unsubscribe link below. If you use the one above, you will stop all of ros-users from receiving updates.
______________________________________________________________________________
ros-users mailing list
ros-users@lists.ros.org
http://lists.ros.org/mailman/listinfo/ros-users
Unsubscribe: <
http://lists.ros.org/mailman//options/ros-users>
(text/plain)