Horst F. Wedde, Arnim Wedig, Anca Lazarescu, Ralf Paaschen und Elisei Rotaru
Model Building and Model Checking under Large-Scale Distributed Interaction
2005-04
In this paper we make a plea for a novel methodology of model checking which, while based on specifications of interaction constrains (and their derived behavior influence on the components involved), exhibits a modeling capability considerably beyond conventional methodologies (Petri Nets, Communicating FSM, etc.) as has been proven before [6]. Although our approach of I–Systems is solely built on 2 primitive interaction relations between components the result mentioned has been achieved through incremental modeling utilizing 3 types of elementary constructions through which e.g. all high-level forms of synchronization can be realized. Since we can cover formal models like Petri Nets our trace semantics originally exposed phenomena of infinity that are adverse to efficient model checking, a consequence of incomplete information. 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 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 thorough and efficient 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.