Starting from the informal specifications of the OM/RR protocol, formal LOTOS descriptions of the protocol and its service were produced and used for subsequent analysis. In order to obtain models of tractable size for verification purposes, a simplified version of the specifications has been considered: the number of service primitives, the number of messages in transit, and the number of associations an OM-protocol entity can do have been fixed, and the error and notification service elements have been omitted.

The LITE toolset has been used to perform simulation and testing of the LOTOS specifications. First, syntax and semantics analysis as well as step-by-step simulation of the LOTOS descriptions were performed using SMILE. Then, several test cases reflecting desired properties of the OM/RR protocol have been constructed and executed using SMILE on the LOTOS specifications. This allowed to detect and correct several misconceptions in the OM/RR protocol.

The CADP toolset has been used to perform verification of the LOTOS specifications. First, CAESAR, ALDEBARAN, and EXP.OPEN were used to generate the models of these specifications (for one association and four messages in transit) in a compositional manner. Then, using ALDEBARAN, the deadlock and livelock freedom of the protocol were checked, as well as the safety preorder inclusion between the protocol and service models.

The results found using the tools increased the confidence in the correct functioning of the OM/RR protocol. However, in order to make the specification and verification activities easier for end-users, a more detailed documentation of the tools would be welcome.