Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2008)
Nov. 10, 2008 to Nov. 14, 2008
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2008.25
We present a process algebra for modeling and reasoning about Mobile Ad hoc Networks (MANETs) and their protocols. In our algebra we model the essential modeling concepts of ad hoc networks, i.e. local broadcast, connectivity of nodes and connectivity changes. Connectivity and connectivity changes are modeled implicitly in the semantics, which results in a more compact state space. Our connectivity model supports unidirectional links. A key feature of our algebra is eliminating connectivity information from the specification of a network, and transferring its complexity to the semantics. We give a formal operational semantics for our process algebra, and define equivalence relations on protocols and networks. We show how our algebra can be applied to prove correctness of an adhoc routing protocol.
ad hoc networks, process algebra, formal verification
W. Fokkink, A. Movaghar and F. Ghassemi, "Restricted Broadcast Process Theory," 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods(SEFM), Cape Town, 2008, pp. 345-354.