We develop a method to validate concurrent layered systems. We define two concepts : model concordance (the model verifies the specification properties) and service consistency (the protocol fulfills its service). We apply our validation method to the Transport protocol (ISO Layer 4). We study loss of connection synchronization in Network layer service and credit requisition in Transport layer protocol. We use High-Level Petri Nets to formally describe the Network service and the Transport protocol. The abstraction concept can be extended to high-level Petri Nets. The correct behavior of the Transport protocol is proved by the model invariants.
