Formal Specification and Verification of WiFiRe protocol
Ch Sudheer Keshav · 2007
WiFiRe stand for WiFi-Rural Extension[1]. There has been a lot of growth in Internet as well as cellular telephony, but it is mostly restricted to only cities in developing countries like India. A number of alternative solutions have been proposed which in theory are suitable for rural areas, but because of their high cost WiFiRe is the best option. WiFiRe is a mixture of the advantages of both 802.11[2] and 802.16[3]. The cost affordability of 802.11 and QoS capabilities of 802.16 are merged to obtain WiFiRe. The WiFiRe MAC is time-division duplex (TDD) over a single 802.11b channel along with a multi-sector TDM mechanism. WiFiRe will be able to provide long range communication by dividing the whole area into sectors, each sector will be having one base station which is directional so that it covers more distance. Formal methods may be used to give a description of the system to be developed, at whatever level(s) of detail desired. This formal description can be used to guide further development activities; additionally, it can be used to verify that the requirements for the system being developed have been completely and accurately specified. Formal methods are mathematically-based techniques for the specification, development and verification of software and hardware systems. Formal methods and testing are a perfect couple, testing and formal verification are both necessary. A formally verified specification is a good starting point for testing. So a formal specification and verification of WiFiRe is required.