Formal modeling and analysis of ad hoc Zone Routing Protocol in Event-B
| Autor: | Chunyan Fu, Kougen Zheng |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Zone Routing Protocol
Static routing Dynamic Source Routing business.industry Computer science Distributed computing ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS Enhanced Interior Gateway Routing Protocol Policy-based routing Wireless Routing Protocol 020207 software engineering 02 engineering and technology Hybrid routing Link-state routing protocol 0202 electrical engineering electronic engineering information engineering business Software Information Systems Computer network |
| Zdroj: | International Journal on Software Tools for Technology Transfer. 21:165-181 |
| ISSN: | 1433-2787 1433-2779 |
| DOI: | 10.1007/s10009-017-0463-4 |
| Popis: | Ad hoc routing protocols are responsible for searching a route from the source to the destination under the dynamic network topology. Hybrid routing protocols combine the features of proactive and reactive approaches. So, the formal specification of a hybrid routing protocol in the dynamic network environment is a challenge. In this paper, we formally analyze the Zone Routing Protocol (ZRP), a hybrid routing framework, using Event-B. We develop the formal specification by the refinement mechanism. It allows us to gradually model the network environment, the construction of routing zones, route discovery based on bordercasting service and routing update. We prove the stabilization property in the inactive environment. In addition, we demonstrate that discovered routes hold the loop freedom and validity in each reachable system state. To present that the formalization is consistent with the informally expressed requirements, we adopt an animator, ProB, to validate our model. Our work provides reference to analyze extensions of the ZRP and other hybrid routing protocols. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink