Runtime verification has gained popularity as a lightweight approach for increasing assurance over systems under scrutiny. By performing checks during execution, it enables dynamic monitoring and alerts for unexpected behaviors, improving reliability and correctness.

Actor-based systems present significant challenges for runtime verification. Properties frequently span multiple actors with complex causal dependencies, while nondeterministic message interleavings can obscure execution semantics. Moreover, most existing monitoring tools are designed for single-process behavior. This paper presents ACTORCHESTRA, a runtime verification framework for Erlang that automatically tracks causality across multi-actor interactions.

The framework instruments Erlang systems that comply with OTP guidelines using targeted code injection. This method establishes the orchestration infrastructure required to track causal relationships between actors without requiring manual modifications to the target system. To facilitate the specification of multi-actor properties, the framework provides WALTZ, a specification language that automatically compiles properties into executable Erlang monitors that integrate with the instrumented system. Three case studies demonstrate ACTORCHESTRA’s effectiveness in detecting complex behavioral violations in real-world actor systems. Performance evaluation quantifies the runtime overhead introduced by the monitoring infrastructure and analyzes the trade-offs between added safety guarantees and execution costs.