Mechanising symbolic controllability

Abstract

Runtime Monitors are computational entities executed alongside programs to observe their behaviour with the aim of reaching a verdict about it. Since monitors are part of the Trusted Computing Base, they are expected to behave correctly; one property that is expected of them is deterministic behaviour. Nevertheless, this criterion is often specified in ambiguous terms. One candidate definition is consistent verdict detections [16]; this property was then characterised further through a symbolic analysis termed symbolic controllability to enable an automated analysis for monitors that involve data. This study investigates whether this symbolic analysis lends itself well for the implementation of a tool that determines whether a monitor exhibits this deterministic behaviour. Subsequently, we implement a tool that automates this symbolic analysis and evaluate it; we establish the worst-case complexity bounds of the designed algorithm and empirically evaluate the implementation. We also investigate multiple optimisation techniques for our implementation to improve its scalability and examine the potential gains incurred by these optimisations against a monitor benchmark.