Semantics, distributed implementation, and formal analysis of KLAIM models in Maude

Emerging distributed systems such as cloud-based services are characterized by computations over different explicit localities, moving code and data, and a high degree of concurrency. KLAIM is a well-established language that can naturally describe such systems. The KLAIM language is process algebra flavored, allows Linda-based asynchronous communication through distributed tuple spaces, and supports explicit localities as well as code and data mobility. In this work we take some first steps in the quest for a correct-by-construction design process for secure and reliable distributed systems. Such a design process is necessary as more and more safety- and security-critical tasks that need to satisfy mission-critical formal requirements are executed in a distributed setting. We use a rewriting-based approach to formally specify and analyze KLAIM specifications of distributed systems. 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 prove that under appropriate weak fairness assumptions all these specifications are stuttering bisimilar and that large classes of logic temporal formulas, namely all CTL⁎∖XCTL⁎∖X formulas, are preserved. By means of an example we show that our approach allows specifying aspects of a distributed system in a Maude-based KLAIM dialect, verifying these specifications using Maude's LTL model checking capabilities, and then executing the verified specifications in a distributed environment. This marks a first step in the quest for a correct-by-construction design process for secure and reliable distributed systems.