Specification of data communication protocols requirements requires a formal approach to ensure that the requirements are correctly and unambiguously specified. This research examines a proposed protocols specification for the movement of bitstream data through space segment by applying a formal definition technique known as the Language of Temporal Ordering System (LOTOS). Successful generation of the LOTOS specification to detail sequence of events and their internal structures in an implementation independent manner clarifies the requirements and provides a framework from which possible cases or events in each process can be tested.

In addition, a LOTOS software tool called HIPPO is used in the research. HIPPO identifies any deadlock that could happen in the protocols and allows sequence of events to be interactively simulated to ascertain of the specification consistency.