Varanus: Runtime Verification for CSP

TL;DR

Varanus is a runtime verification tool that monitors autonomous systems against CSP specifications, enabling reuse of existing models and demonstrating efficient performance in detecting specification violations.

Contribution

This paper introduces Varanus, the first runtime verification tool for CSP, allowing real-time monitoring of autonomous systems using existing CSP specifications.

Findings

Varanus can synthesize monitors in roughly linear time.

It checks each event in roughly constant time.

It effectively detects violations in a simulated robotic system.

Abstract

Autonomous systems are often used in changeable and unknown environments, where traditional verification may not be suitable. Runtime Verification (RV) checks events performed by a system against a formal specification of its intended behaviour, making it highly suitable for ensuring that an autonomous system is obeying its specification at runtime. Communicating Sequential Processes (CSP) is a process algebra usually used in static verification, which captures behaviour as a trace of events, making it useful for RV as well. Further, CSP has more recently been used to specify autonomous and robotic systems. Though CSP is supported by two extant model checkers, so far it has no RV tool. This paper presents Varanus, an RV tool that monitors a system against an oracle built from a CSP specification. This approach enables the reuse without modifications of a specification that was built, e.g during the system's design. We describe the tool, apply it to a simulated autonomous robotic rover inspecting a nuclear waste store, empirically comparing its performance to two other RV tools using different languages, and demonstrate how it can detect violations of the specification. Varanus can synthesise a monitor from a CSP process in roughly linear time, with respect to the number of states and transitions in the model; and checks each event in roughly constant time.