From FSL
Revision as of 23:08, 27 May 2014 by Cerdoga2 (Talk | contribs)

Jump to: navigation, search

ROSRV is a runtime verification framework for the Robot Operating System (ROS) [1]. ROS is an open-source framework for robot software development, providing operating system-like functionality on heterogeneous computer clusters. With the wide adoption of ROS, its safety and security are becoming an important problem. ROSRV integrates seamlessly with ROS and works as a transparent monitoring infrastructure that intercepts the commands and messages passing through the system and performs monitoring actions upon events of interest. Safety and security properties can be defined in a formal specification language, and are ensured by monitors generated automatically from specifications.


Getting Started




To generate monitors out of event specifications, first you have to compile the ROSMOP tool.

Go to rosmop directory and call


For the monitor generation and the compilation of RVMaster with the generated code, call the script rosmop with event specification(s) as input. For example:

rosmop monitors/landshark_monitors/


rosmop monitors/turtlesim/color.rv


rvcore: runs ROSMaster and RVMaster

rvsim: runs the LandShark simulator (requires Webots)
(to run turtlesim instead, use: rosrun turtlesim turtlesim_node)

rvjoystick: runs the joystick controller
(to run the turtlesim controller instead, use: rosrun turtlesim turtle_teleop_key)

Monitoring options


-enable: enables given monitor(s)
-disable: disables given monitor(s)
-list: lists active monitors
-rvstate: lists the status of RVMaster regarding monitors

Event Specification

All the specifications are provided by users. ROSRV generates C++ code automatically based on those specifications. Each event generates one call back method and all the call back methods are registered by RVMaster. Parameters of events are treated as references to fields in monitored messages, so users can modify messages in event handler code. Event handlers (i.e. actions) are inserted in call back methods and called by RVMaster at runtime. Event specification names are used to identify the monitors. By using those names, one can enable or disable desired monitors, and hence control which events take place.

Basic form of a user-defined event specification is the following:

#include <library>
int i;
bool b;
event event1(parameters) topic messageType '{pattern}'
//action code

The following event specification defines the monitor which makes sure the robot doesn't shoot itself.

In this specification, there are two events, checkPosition and safeTrigger, which have their own parameters and topics. On each topic, there can only be a certain type of message sent and received, which is also provided in the event signature. checkPosition event checks whether the gun is at a safe position to trigger, i.e. position > -0.45 (not pointing at itself). It listens to topic /landshark/joint_states with the message type sensor_msgs/JointState. The fields of the message type can be accessed by providing the parameters of interest as done here; there are two arrays, name and position, which are bound to variables N and P, respectively. These parameters are used in the action code of the event to check the validity of the message content.

For clarity, please check out our demo.

#include <stdint.h>
safeTrigger() {
bool isSafeTrigger = false;
event checkPoint(std::string monitored_name, double monitored_position) /landshark/joint_states sensor_msgs/JointState '{name[1]:monitored_name, position[1]:monitored_position}'
if(monitored_position > -0.45){
isSafeTrigger = true;
ROS_INFO("Safe to trigger");
isSafeTrigger = false;
ROS_INFO("Not safe to trigger");
event safeTrigger() /landshark_control/trigger landshark_msgs/PaintballTrigger '{}'
ROS_WARN("Monitor: Not allowed to trigger in this pose!");

Access Control

ROSRV enforces access control based on a user-provided specification of access policies as input configuration. On receiving any XMLRPC request from nodes, RVMaster decides whether the request is allowed to go to the ROSMaster according to the specification.

The policies are currently categorized into four different sections. Under each section, the access policy is written as a key followed by an assignment symbol and a list of values.

[Nodes]: key = node name, value = machine identity allowed to create the specified nodes

[Subscribers]: key = topic name, value = node identity allowed to subscribe to the topic

[Publishers]: key = topic name, value = node identity allowed to publish to the topic

[Commands]: key = command name, value = node identity allowed to perform the command

The following is a sample access control policy for LandShark:

# Aliases
localhost =
certikos = ip1 ip2 ip3 ip4
ocu = ip5 ip6 ip7 ip8
# by default, allowed to create any node
default=localhost certikos
/landshark_control/trigger= ocu
default = localhost certikos
/landshark/gps = ocu
# Commands: full access
getSystemState = localhost certikos ocu
# Commands: limited access
lookupNode = localhost certikos
# Commands: local access only
shutdown = localhost


Watch our demo to see how the monitors interact with the robot LandShark [2]:


[1] ROS

[2] The LandShark UGV is a product of Black-i Robotics

Personal tools