Usage

In order to use the tool, we need to define a monitor configuration, such as the following:

path: /path/to/monitor/workspace/src/ # path to the ros workspace of the monitor package

monitors: # list of generated monitors
- monitor:
    id: my_monitor # monitor id
    log: ./log.txt # file where the monitor will log the observed events
    silent: False # the monitor prints info during its execution
    oracle: # the oracle running and ready to check the specification
        port: 8080 # port where the oracle is listening
        url: 127.0.0.1 # url where itthe oracle is listening
        action: nothing # action performed by the oracle
    topics: # list of topics this monitor is going to intercept
        - name: my_topic # name of the topic
        type: std_msgs.msg.String # type of the topic
        action: log
        qos_reliability: reliable  # topic reliability
    services: # list of services the monitor intercepts
        - name: my_service # name of the service
        type: std_msgs.msg.String # type of the service
        action: log
    actions: # list of actions the monitor intercepts
        - name: my_action # name of the action
        type: custom_action_interfaces.action.MyAction # type of the action
        action: log

Then, we need to generate the corresponding monitor, by invoking the moon_generator command.

$ moon_generator --config-file /path/to/monitor_config.yaml

Now we need to build the newly created ROS package, so we run

$ cd /path/to/monitor/workspace
$ colcon build

Next, we need to define a property to be verified on the monitored topics and/or services, such as

import oracle

# property to verify
PROPERTY = "historically{p}"

# declaration of predicates used in the property (initialization at time 0)
predicates = dict(
    time = 0,
    p = True,
)

# function to abstract a dictionary (obtained from Json message) into a list of predicates
# the behavior of the function must be defined by the user depending on the property and topic/service message
def abstract_message(message):
    predicates['time'] = message['time']
    predicates['p'] = message['p']
    return predicates

The PastMTL property needs to be defined as a string assigned to the PROPERTY variable, following the Reelay syntax.

Then, we need to run the oracle by specifying the property and whether the time events are evenly spaced out or not, by setting either the --dense or --discrete flag.

$ moon_oracle --online --property /path/to/prop --port 8080 --dense

We can now run the monitor, with

$ cd /path/to/monitor_ws
$ source install/setup.bash
$ ros2 run monitor my_monitor

In case any action monitors were defined, we need to also start the corresponding node in the same workspace

$ ros2 run my_action_monitor my_action_monitor

Now the monitor will be running, and when the monitored channel is running, it will send messages to the oracle, which will provide an evaluation of the property.