Restricted Broadcast Process Theory Algebraic specification and verification of MANETs [back to the homepage]

Description

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.

Download

• The source code is available at github

Contributers

• Pooyan Behnamghader
• Yeganeh Khashkhashi Moghaddam
• Zahra Ghaed
• Peyman Mahdian

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.