MESA: Message-Based System Analysis(ARC-18229-1)

MESA, which stands for MEssage-based System Analysis, is a framework that provides runtime verification of large distributed systems in a nonintrusive manner. It checks a trace of the system under test against properties of interest, and if a property is violated, it issues an error along with a counter example. A trace is a sequence of messages entailing information about a run of the system. MESA leverages RACE, which is a platform for instantiating and running highly concurrent and distributed systems, to provide connectivity to and retrieve information from the system under test. Using existing domain specific languages, TraceContrance and Daut, It allows for formal specification of properties in state machines and linear temporal logic formulas. MESA is written in Scala, and employs the actor programming model, as implemented in the Akka framework. Finally, using asynchronous communicating actors to capture properties of interest, it allows for decentralized monitoring of the system.