Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2008)

Nov. 10, 2008 to Nov. 14, 2008

ISBN: 978-0-7695-3437-4

pp: 345-354

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2008.25

ABSTRACT

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.

INDEX TERMS

ad hoc networks, process algebra, formal verification

CITATION

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.

doi:10.1109/SEFM.2008.25

CITATIONS