Horst F. Wedde, Arnim Wedig, Anca Lazarescu, Ralf Paaschen und Elisei Rotaru
Modeling and Analyzing Large-Scale Distributed Interaction
2005-03
Due to the (partially) autonomous behavior of their components, large-scale distributed systems impose intricate problems on their formal modeling and analysis. E.g. the complexity as much as their sheer size suggest an incremental modeling strategy. Also, analyzing the behavior of big systems is clearly limited when done on the basis of formal semantics which are typically infinite in general, like trace semantics. In earlier papers we had presented I–Systems as a formal approach completely based on 2 elementary interaction relations between components. We had proven that this tool while allowing for efficient incremental modeling strategies in-the-large, is more powerful than traditional modeling methodologies (Petri Nets etc.). In this paper we present a novel abstract set of action rules respecting, and borrowing from, the interaction relations. These yield the same trace semantics as the earlier implementation-oriented behavior axioms. We also define a finite structure, the behavior graph of an I-System. The main result is that the corresponding trace semantics which in general is infinite, and the behavior graph are “equivalent” in that they describe the same behavior. The behavior graph appears as a convolution of the trace semantics. We demonstrate the advantage of this result for a formal analysis in an example which, despite the small size of its formal presentation, has a rich and complex behavior structure. Perspectives for future research are outlined.