Runtime verification program side‐effects in OCaml

Abstract

The paper aims to ensure the correctness of functional programs, written in OCaml. Despite being known for its functional programming features, OCaml provides support for imperative programming through the use of references, which are mutable variables enabling the sharing of states. However, their use in functional programming can introduce sofware bugs typically associated with non‐deterministic behaviour. The paper addresses these challenges through runtime verification, a technique that monitors OCaml program execution and checks for adherence to safety properties. This technique involves instrumenting the program to generate a trace that captures information about the events occurring during the OCaml program execution, including reads, writes, and references initalisations. The synthesised trace will be passed to monitors to enable runtime verificaton and analysis of critical events that capture program behaviour. The monitor will leverage as a formal method to detect and fag violations in real‐tme, ensuring correctness and robustness of the System under Scrutiny (SuS). To formally specify the properties, this project aims to verify using the sub‐logic of safety fragment of Hennessy‐Milner logic with recursion (sHML) [1], which is a syntactic subset of Hennessy‐Milner Logic with recursion (HML) [2]. This logic is used to specify and implement safety properties for our Runtime Verifcaton (RV) tool detectEr. Using sHML to express the properties to be checked, the project aims to generate synthesised properties that capture the essential program behaviour aspects [3], ensuring correctness. The project uses a monitoring algorithm to check the synthesised propertes against the program’s trace during executon. In order to ensure correctness, lists of events must undergo formal verifcaton. The monitoring algorithm then applies runtme analysis techniques to detect potental violatons of system propertes. Based on the analysis results, boolean fags are generated to indicate the presence or absence of a violaton. This simplifes the process of locatng and reportng any violatons that may arise in the OCaml program, thereby ensuring program correctness, robustness, and overall quality of the running SuS.