RoboChart: modelling and verification of the functional behaviour of robotic applications

2 min read

RoboChart is a state-machine language for robot controllers: a small profile of UML state machines with an explicit robotic platform (its variables, events and operations), controllers that talk synchronously inside and asynchronously between each other, a fully specified action language, and timing primitives for budgets and deadlines. Every model gets a formal semantics in CSP (and tock-CSP for time), so the FDR refinement checker can prove deadlock, livelock and timelock freedom, or state reachability. The Eclipse tool RoboTool generates the CSP and the assertions automatically. The paper gives the metamodel, the well-formedness rules and the full semantics.

Findings

  • Case studies from the literature: a foraging robot with dynamic task partitioning, a chemical detector, an autonomous detector, a transporter and the alpha algorithm (a swarm aggregation rule).
  • Timed checks with FDR are fast at this scale: the largest model (alpha algorithm) has 4427 states and 10,405 transitions, with deadlock checking in 0.37 s and the longest check 0.48 s. Compilation takes up to 15.65 s (transporter).
  • Timed semantics expose hidden assumptions. In the Movement machine of the autonomous chemical detector, a “during” action that calls a random-walk operation creates timelocks unless the platform accepts the call at all times and finishes it in zero time.

Limits

  • By design there are no parallel states; concurrency comes from separate machines and controllers. The authors list as future work a detailed model of the environment and of continuous dynamics (taking ideas from hybrid automata), probabilistic choice, and automatic visualisation of FDR counterexamples, which today need manual reading.
  • Code generation covers only a subset of the notation, and correctness of generated simulations and code is future work. So a verified model can still drift from what runs on the robot.
  • The verified properties are about the controller’s own logic. Sensor faults or attacks appear only if someone models them as events.

Relevance

RoboChart gives robot state machines a precise meaning, so properties such as timelocks and unreachable states can be checked before deployment. For the wider survey see Luckcuck et al., and for checking properties on the running robot see runtime monitoring.