Threefold Analysis of Distributed Systems: IMDS, Petri Net and Distributed Automata DA3

TL;DR

This paper presents a comprehensive analysis of distributed systems using the IMDS formalism, Petri nets, and DA3 automata, enhancing specification, verification, and simulation methods without global configuration calculations.

Contribution

It introduces DA3 automata for simulation, links IMDS with Petri nets for structural analysis, and integrates these formalisms within the Dedan verification environment.

Findings

DA3 automata enable simulation without global configuration computation

Petri nets provide structural analysis of IMDS models

The integrated approach improves distributed system verification

Abstract

Integrated Model of Distributed Systems is used for specification and verification of distributed systems. In the formalism, a system is modeled as a set of servers' states and agents' messages. The operation of a system is modeled as actions converting global system configuration (a set of states and messages) to a new configuration. The formalism is used in Dedan verification environment, in which specification and verification of distributed systems is performed. Equivalent Petri nets are used for structural analysis. For the graphical specification and simulation of distributed systems, Distributed Autonomous and Asynchronous Automata (DA3) are invented. Such simulation does not require calculation of global configuration space of a system. Two forms of DA3 are shown: Server-DA3 (SDA3) for the server view and Agent-DA3 (ADA3) for the agent view.