Talk "Semantics and Analysis of KLAIM Models in Maude"

by Martin Wirsing

Thu, 09 January 2014 at 09:00 am in Theddingworth near Leicester, UK

Joint work with: J. Eckhardt, T. Mühlbauer, and J. Meseguer

Abstract: The coordination language KLAIM is well-suited for modelling message-passing-based distributed systems. It is based on a distributed Linda-like memory model and features explicit localities as well as remote access to memory. In this work we use a rewriting-based approach to formally specify and analyze KLAIM and its semantics. In particular we: (i) specify the reduction semantics of KLAIM in Maude, (ii) extend the Maude-based specification by making messages first-class citizens, and (iii) describe a second extension that allows true distributed execution of Maude-based KLAIM specifications. We analyze the relationships between these specifications and show that the Maude implementation of KLAIM is bisimilar to the reduction semantics of KLAIM, the distributed extension is stuttering bisimilar with the message-extension whereas the message extension is only a stuttering simulation of KLAIM. To our knowledge the Maude implementation is the first provably correct implementation of KLAIM.