Design and Implementation of a Protocol for the SagaMAS Framework to Manage Distributed Transactions in Microservices Architecture

Abstract

SagaMAS is a framework that integrates multi-agent sys- tems (MAS) with microservices to coordinate long-lived dis- tributed transactions. While its original formulation laid out the architectural vision, it deferred the formal specification of its transaction protocol. This paper addresses that gap by defining the SagaMAS protocol through six core rules: initiation, commit-then-report, dependency management, time- outs and retries, compensation, and termination without global commit. The protocol is formally specified in PROMELA and verified using the SPIN model checker against safety, liveness, and responsiveness properties. Verification results confirm that SagaMAS avoids deadlocks, maintains safety, and guarantees eventual termination. By contributing a formally verified transaction protocol, this work reinforces the Saga- MAS framework and lays the foundation for future empirical benchmarking against established orchestration platforms such as Axon Framework, Eventuate Tram, and Netflix Conductor.