Protocol Validation and Implementation:
   A Design Methodology Using LOTOS and ROOM

Neil HART Master Thesis
University of Ottawa, 1999.

Abstract

Formal methods have been proposed as a means of expediting the creation of
reliable software. The use of formal methods allows for clear and unequivocal
specification of a system's design, and makes possible a form of prototyping
that allows for formal validation against system requirements.  However, the
adoption of formal methods by industry has so far been slow.

It is proposed that one of the obstacles to the adoption of formal methods is
the difficulty of bridging the gap between a formally-specified system and a
working implementation. If this gap is too wide, the advantages of formal
specification will be lost in the transition to implementation.

The methodology described in this thesis attempts to close this gap by
demonstrating how a system may be described using LOTOS (Language Of Temporally-
Ordered Specifications) and validated against requirements using two techniques:
composition with agent scenarios and temporal logic model checking. The
methodology then allows for the derivation of a model in the ROOM (Real-Time
Object-Oriented Modelling) notation, which may be automatically converted to an
implementation in the C++ programming language.

The methodology is illustrated with two small case studies. The first is the
GPRS Tunnelling Protocol, used for transmitting protocol data units within the
network of the General Packet Radio Service. The second study concerns
authentication of users of the POP3 Internet mail protocol and demonstrates
inheritance in LOTOS.  Together, these case studies illustrate the salient
points of the design methodology.