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

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.

10 pages, 5 figures, 1 table

References in corpus (6)

• Serializing the Parallelism in Parallel Communicating Pushdown Automata Systems
• Rybu: Imperative-style Preprocessor for Verification of Distributed Systems in the Dedan Environment
• Evaluation of Temporal Formulas Based on "Checking By Spheres"
• On distributed monitoring of asynchronous systems
• Improving Resilience of Autonomous Moving Platforms by Real Time Analysis of Their Cooperation
• Communication Dualism in Distributed Systems with Petri Net Interpretation