Formal Runtime Monitoring of the MASCOT v.6 system from its safety designs
As part of planned upgrades to the MASCOT system, a new safety assessment and design have been produced. We use this safety design to build a specification of the new MASCOT safety subsystem. The specification is written in the formal specification language CSP, which is mathematically-based and amenable to a variety of formal methods – in this case, exhaustive model checking.
We have built a new runtime verification toolchain called Varanus to interface with the MASCOT system, interpret its behaviour, and check it against the specification. The toolchain currently performs offline verification, by processing logs of system updates. The current version of the MASCOT system does not yet produce the information required to monitor the safety properties.
This runtime verification approach is effective at bridging the reality gap between design-time assumptions and run-time environments; which is especially useful for robotic systems, because they operate in the real-world. The monitoring is based on the system’s safety requirements, therefore providing traceability of these properties into a system component.