Automated checking for deterministic monitor behaviour

Abstract

Monitors are computational entities typically instrumented with an other computational entity referred to as a system to observe its executions with the intent of collecting system information or verify its behaviour [Fra16]. Monitors are central to several software engineering techniques including monitor-oriented programming and runtime verification, a lightweight verification technique where monitors observe the trace produced during a system run. Monitors are often considered to form part of the Trusted Computing Base (TCB), and as a result are expected to be correct. A frequent correctness requirement is often assumed that they should exhibit deterministic behaviour. One such definition of determinism is through the notion of controllability [Kla09, Dor01]. Which, in discrete event systems, refers to the ability to steer a (passive) entity to designated terminal states via a series of admissible controls. In [Fra17a], Francalanza develops a coinductive definition for controllability, that can be used to automate the process of checking a monitor description for determinism. He also defines a second definition for determinism, termed symbolic controllability, which uses symbolic events and conditions instead of concrete events. Francalanza conjectures that both definitions for controllability and symbolic controllability are implementable and also claims that an implementation based on the latter can analyse more monitors in an e ective manner. In the presented work, we set out to verify the implementability claims for controllability and its symbolic counterpart by producing algorithms for the formal definitions of [Fra17a]. Moreover, we investigate the claim that symbolic controllability is more e ective in detecting monitor determinism when compared to the other definition. We shall be verifying the claims made in [Fra17a] via a number of pathological examples.