Formalization of Semantics of Systems with Unreliable Agents by Means of Nets of Active Resources

摘要

A new method for modeling distributed systems-nets of active resources-is presented. The expressive power of this formalism is similar to that of ordinary Petri nets, but its syntax relies on a different modeling principle: instead of partitioning model components (nodes of the graph) into agents and resources (transitions and places), partitioning of the ways of interaction (arcs of the graph) in terms of production and consumption is introduced. Direction of an arc determines whether the interaction is active or passive: one and the same component upon different firings may play role of both an agent and a resource. In nets of active resources and their syntactic extensions, there appears an opportunity for convenient formalization of various semantic properties, such as simultaneous work of agents, agent blocking, redundancy of the number of agents, a possibility of replacement of an unreliable node by a reliable one, and the like. A method for constructing distributed applications based on dynamically configured sets of executable modules is considered. It is shown that the use of nets of active resources allows one to specify their structure, as well as to formulate properties of such systems, in a natural way.