Nguyen, Quoc The2014-03-142014-03-141989etd-06122010-020641http://hdl.handle.net/10919/43293Specification 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.vi, 127 leavesBTDapplication/pdfenIn CopyrightLD5655.V855 1989.N487Computer simulationMathematical modelsProtocols specification and validation for the movement of Grades 2 and 3 Bitstream data through the Virtual Channel Link Control layer of the return link of the CCSDS Principal Network (CPN)Thesishttp://scholar.lib.vt.edu/theses/available/etd-06122010-020641/