git-afsantos / haros

H(igh) A(ssurance) ROS - Static analysis of ROS application code.
MIT License
191 stars 37 forks source link

Provide a language for node/msg properties #28

Closed git-afsantos closed 3 years ago

git-afsantos commented 5 years ago

Such a language could be used to automatically generate property-based tests, for instance, without having to write code.

These properties could be embedded into the YAML project files, within their own section. Example:

%YAML 1.1
---
project: example
packages: []
properties:
  msg:
    pkg/msg: []
  node:
    pkg/node: []

msg properties would be message field invariants, applicable to every message independently of the context, e.g. enum fields.

node properties are applicable to a node's behaviour, mostly regarding what the node publishes and what it expects to receive, in an initial approach.

Example properties:

publish(msg, topic) within 0.1 s where field1 < 1, field2 < 2

publish(m, topic) [< 100 ms] {f1 < 1, f2 < 2, f3 < 3}

receive(e, ~events/bumper) {state = PRESSED}
  >> publish(c, ~cmd_vel) [< 100 ms] {linear.x < 0.0}