Modeling and analysis of concurrent systems using contour/transition-nets

This dissertation introduces a model for parallel computation, the Contour/Transitition model, which blends the strengths of transition-based systems (concurrency, conflict, and synchronization) with the strength of contour-based systems (control and data absraction) . By using contour/transition-nets to model computer communication protocols, a basis is provided for the formal modeling and analysis of cocurrent systems. The contour/transition model adds three notions to Petri net theory: invocations which corresponds to Petri net procedures: colors which model multiple instantiations of nets; and contours which permit scoping mechanisms. This dissertation develops an extension to Keller's invariant-method for parallel computation that is useful for proving properties of contour/transition-nets. The usefulness of contour/transisition-nets is demonstrated by a model of initial connection handling (a three-way handshake) for a protocol that offers virtual-circuit service (the DoD Transmission Control Protocol)