Description and validation of the Internet Stream Protocol (ST2+) using SDL/MSC

We propose a formal description of a large subset of the Internet Stream Protocol version 2 (ST2+) protocol using the Specification and Description Language (SDL) and Message Sequence Charts (MSC). ST2+ is an experimental resource reservation protocol developed by the Internet task force. The checking of general properties of the model were performed using the ObjectGEODE tool. We have found that all the ST2+ protocol properties that we tested succeeded the verification. In addition, we have found that the use of SDL/MSC simplifies the description and validation of the protocol, and facilitates the possibility for future extensions of our model.