The success of any today large-scale software depends largely on the techniques applied to different phases of its whole life cycle. Various formal methods arid testing methods are developed to be applied to the specification phase and testing phase. Based on,the author's own experience as a member of a team implemeriting the Information Search and Retrieval Protocol, the Z39.50, this thesis explores application of formal methods and a methodology from a practical point of views.