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

Jonas Eckhardt, Tobias Mühlbauer, José Meseguer, Martin Wirsing

Research output: Contribution to journalArticle

Abstract

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∗\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.

Original languageEnglish (US)
Pages (from-to)24-74
Number of pages51
JournalScience of Computer Programming
Volume99
DOIs
StatePublished - Mar 1 2015

Keywords

  • Correct-by-construction
  • Distributed system
  • Formal analysis
  • KLAIM
  • Rewriting logic

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Semantics, distributed implementation, and formal analysis of KLAIM models in Maude'. Together they form a unique fingerprint.

  • Cite this