Restricted Broadcast Process Theory (RBPT) was introduced for formal modeling and verification of Mobile Ad Hoc Networks (MANETs) in an algebraic way. In this project, a tool that checks the static semantics of a given specification was developed. Furthermore, it linearizes the algebraic specifications using the sound axioms of RBPT. To this aim, two approaches were followed. In the first approach, the specifications are translated into the functional programming language Haskell, which in turn handles the linearization. In the second, linearization was implemented on the syntax tree translations of the specifications.



Related Publications

  1. F. Ghassemi, W. Fokkink, and A. Movaghar, "Restricted Broadcast Process Theory", in Proc. 6th Conference on Software Engineering and Formal Methods - SEFM'08, Cape Town, pp. 345-354, IEEE , 2008.
  2. F. Ghassemi, W. Fokkink, and A. Movaghar, "Equational Reasoning on Mobile Ad Hoc Networks", Fundamenta Informaticae, Vol. 105, No. 4, pp. 375-415, 2010.
  3. F. Ghassemi, W. Fokkink, and A. Movaghar,"Verification of mobile ad hoc networks: An algebraic approach", Theoretical Computer Science, Vol. 412, No. 28, pp. 3262-3282, 2011.
  4. F. Ghassemi and W. Fokkink, "Reliable Restricted Process Theory", Accepted in Fundamenta Informaticae, To appear.