| of the Open Systems Interconnection Reference Model (OSI-RM) developed using Object-Oriented modeling principles permitting it to serve as a re-usable platform in supporting the development of simulations and formal methods applied to layered network protocols. A simulation of the object model using MODSIM III was developed and Prototype Verification System (PVS) was used to show the applicability of the object model to formal methods by formally specifying and verifying a Global Systems for Mobile communications (GSM) protocol. This application has proved to be successful in two aspects. The first was showing the existence of discrepancies between informal standard protocol specifications, and the second was that communication over the layered GSM network was verified. Although formal methods is somewhat difficult and time consuming, this research shows the need for the formal specification of all communication protocols to support a clear understanding of these protocols and to provide consistency in their implementations.; A domain for the application of this model is mobile cellular telecommunications systems. Mobile Communications is one of the most rapidly expanding sectors of telecommunications. Expectations of what a mobile cellular phone can do have vastly increased the complexity of cellular communication networks, which makes it imperative that protocol specifications be verified before implementation. |
