A Formal Approach to the Engineering of Domain-Specific Distributed Systems

TL;DR

This paper reviews formal methods and languages for designing, programming, and verifying various classes of distributed systems, emphasizing domain-specific approaches and their practical applications.

Contribution

It provides a comparative overview of four formal languages for distributed systems, detailing their design, semantics, and verification techniques in a unified framework.

Findings

Four formal languages are analyzed: Klaim, Cows, Scel, AbC.

Each language's syntax, semantics, and modeling capabilities are described.

Practical examples demonstrate their application to distributed system scenarios.

Abstract

We review some results regarding specification, programming and verification of different classes of distributed systems which stemmed from the research of the Concurrency and Mobility Group at University of Firenze. More specifically, we examine the distinguishing features of network-aware programming, service-oriented computing, autonomic computing, and collective adaptive systems programming. We then present an overview of four different languages, namely Klaim, Cows, Scel and AbC. For each language, we discuss design choices, present syntax and semantics, show how the different formalisms can be used to model and program a travel booking scenario, and describe programming environments and verification techniques.