Description, Based On The Ip Protocol In The Form Of The Process Operator

With the further development of computer networks, communication networks, distributed systems and communication protocols are more and more complicated. Formal description technology plays an indispensable role in the network protocol design. LOTOS - as one of the ISO standards of FDT, is designed for distributed systems, especially for communication service and communication protocol.In this thesis, the application of LOTOS technology to network communication protocol design is studied. The formal description technology based on LOTOS, the formal transformation, the formal validation and implemenation are generalized. Constructions of communication service and communication protocol, transformation from service specification into protocol specification based on bisimulation equivalence are also stated in detail. Application of LOTOS specification styles, architecture concept and stepwise refinement design in service and protocol design is studied as an emphasis.This thesis mainly includes four parts:First, the application field of ADT in protocol project, the background and the development of LOTOS technology are briefly introduced and the foundation of LOTOS language is described.Second, the application spectrum of technology based on LOTOS in network protocol design is discussed in detail, which includes LOTOS specification styles, LOTOS transformation, LOTOS validation, LOTOS implementation, ELOTOS and LOTOS toolkit, etc.Third, the composition of communication model, construction of service specification and protocol specification, and the approach of transform service specification into protocol specification are described.Finally, the application method of LOTOS specification styles in network services and protocol design, the concept of formal structural model and its design approach, the transformation of LOTOS specification to C or C++ are produced. Stepwise refinement design is presented and applied to an example for systemic design of a network gateway protocol.