Search papers, labs, and topics across Lattice.
This paper introduces ACTORCHESTRA, a runtime verification framework for Erlang actor-based systems that automatically tracks causality across multi-actor interactions using code injection. The framework includes WALTZ, a specification language that compiles properties into executable Erlang monitors. Case studies on real-world actor systems demonstrate ACTORCHESTRA's effectiveness in detecting complex behavioral violations, while a performance evaluation quantifies runtime overhead.
Automatically tracking causality across actors exposes hidden behavioral violations in real-world Erlang systems, without requiring manual code modifications.
Runtime verification has gained popularity as a lightweight approach for increasing assurance in systems under scrutiny. Performing runtime checks enables dynamic monitoring and alerts for unexpected behavior, thereby 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 via 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 ease 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. A performance evaluation quantifies the runtime overhead of the monitoring infrastructure and analyzes the trade-offs between added safety guarantees and execution costs.
