Formally specified monitoring of temporal properties

TLDR

MaC bridges the gap between formal specification of designs and testing of implementations, which lacks formality. The paper presents the Monitoring and Checking (MaC) framework, an overview of its languages for monitoring scripts and requirements, and a prototype implementation for Java systems, aiming to provide runtime assurance of real‑time system correctness. MaC performs monitoring based on formal specifications of high‑level requirements, separates implementation‑dependent monitored objects from these specifications, and automatically instruments executable code.

Abstract

We describe the Monitoring and Checking (MaC) framework which provides assurance on the correctness of an execution of a real-time system at runtime. Monitoring is performed based on a formal specification of system requirements. MaC bridges the gap between formal specification, which analyzes designs rather than implementations, and testing, which validates implementations but lacks formality. An important aspect of the framework is a clear separation between implementation-dependent description of monitored objects and high-level requirements specification. Another salient feature is automatic instrumentation of executable code. The paper presents an overview of the framework, languages to express monitoring scripts and requirements, and a prototype implementation of MaC targeted at systems implemented in Java.