Difference between revisions of "ROSRV"

From FSL
Jump to: navigation, search
(Download)
Line 21: Line 21:
  
 
=== Run ===
 
=== Run ===
 +
 +
<font face=Courier>rvcore</font>: runs rosmaster and rvmaster
 +
 +
-<font face=Courier>roscore -p 12345</font>
 +
 +
-<font face=Courier>./rvmaster.sh</font>
 +
 +
 +
<font face=Courier>rvsim</font>: runs the LandShark simulator (requires Webots)
 +
 +
<font face=Courier>rvjoystick</font>: runs the joystick controller
 +
  
 
=== Monitoring options ===
 
=== Monitoring options ===
  
<font face=Courier>-enable</font>: enables given monitor(s)
+
<font face=Courier>rosrv</font>
 +
 
 +
: <font face=Courier>-enable</font>: enables given monitor(s)
  
<font face=Courier>-disable</font>: disables given monitor(s)
+
: <font face=Courier>-disable</font>: disables given monitor(s)
  
<font face=Courier>-list</font>: lists active monitors
+
: <font face=Courier>-list</font>: lists active monitors
  
<font face=Courier>-rvstate</font>: lists the status of RVMaster regarding monitors
+
: <font face=Courier>-rvstate</font>: lists the status of RVMaster regarding monitors
  
  

Revision as of 21:06, 21 March 2014

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.

Contents

Getting Started

Download

rvmaster

Compile

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

Go to rosmop directory and call

ant

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

rosmop monitors/landshark_monitors/


Run

rvcore: runs rosmaster and rvmaster

-roscore -p 12345

-./rvmaster.sh


rvsim: runs the LandShark simulator (requires Webots)

rvjoystick: runs the joystick controller


Monitoring options

rosrv

-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.

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

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

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.

The following event specification defines the monitor which makes sure the robot doesn't shoot itself. 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_name=="turret_tilt")
{
if(monitored_position > -0.45){
isSafeTrigger = true;
ROS_INFO("Safe to trigger");
}else{
isSafeTrigger = false;
ROS_INFO("Not safe to trigger");
}
}
>>
 
event safeTrigger() /landshark_control/trigger landshark_msgs/PaintballTrigger '{}'
<<
if(!isSafeTrigger)
{
ROS_WARN("Monitor: Not allowed to trigger in this pose!");
return;
}
>>
}


Demo

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

References

[1] ROS

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

Personal tools
Namespaces

Variants
Actions
Navigation