Verification of Mobile Ad hoc Network Processes with Data

Q: How can I download an article?

To download an article from SID, first log in to the site, search for the article title, and click on the 'Download Article' option.

Q: How can I download an ISI article?

To download an ISI article on SID, enter the keyword or article title in the search bar, view the relevant results, click on the desired article, and select the 'Download Article' option.

Q: How can I access the SID database?

To access the SID database, visit SID.ir, create an account, and log in to access scientific resources.

Q: Is downloading articles from SID free?

Some articles on SID are available for free, while others require payment. Details are specified on the article's page.

GHASSEMI FATEMEH

مرکز اطلاعات علمی Scientific Information Database (SID) - Trusted Source for Research and Academic Resources

Journal Paper

Paper Information

Journal: THE CSI JOURNAL ON COMPUTER SCIENCE AND ENGINEERING Year:2018 | Volume:15 | Issue:2 Page(s): 44-52

Download Full-Text

View:

174

Download:

Cites:

Information Journal Paper

Title

Verification of Mobile Ad hoc Network Processes with Data

Author(s)

GHASSEMI FATEMEH | Issue Writer Certificate

Keywords

Model checking

Ad hoc networks

Topology-dependent property

State-space explosion

Abstract

Topology-dependent behavior of wireless communication makes the modeling and verification of Mobile Ad hoc networks (MANETs) more complicated. Reliable Restricted Broadcast Process Theory (RRBPT) was introduced to specify and analyze MANETs in an algebraic approach. Constrained Action Computation Tree Logic (CACLT), interpreted over the semantics of RRBPT, allows to specify topology-dependent properties of MANETs. However, Model checking of CACTL formulae is restricted to MANETs with a small number of nodes or finite datatypes. Having an algebraic specification, the problem of Model checking of CACTL properties can be reduced to solving Boolean equations, as an intermediate formalism. This technique has been followed in the mCRL2 toolset to verify -calculus properties extended with data. Having a sound translation from RRBPT to mCRL2, we can use its toolset to verify data-dependent properties of MANET processes with infinite state, data-dependent behaviors. By treating the topology-dependent behavior of CACTL modals as data, we can also verify topology-dependent behavior of MANETs. To this aim, we provide a sound translation from CACTL formulae to first order modal -calculus expressions. Our translation takes advantage of the formal treatment of data and parametrized propositional variables in the mCRL2 process and property specifications respectively to address the topology-formulae part of CACTL expressing multi-hop constrains over the topology.

Cites

No record.

References

No record.

Cite

APA: Copy

GHASSEMI, FATEMEH. (2018). Verification of Mobile Ad hoc Network Processes with Data. THE CSI JOURNAL ON COMPUTER SCIENCE AND ENGINEERING, 15(2), 44-52. SID. https://sid.ir/paper/775824/en

Vancouver: Copy

GHASSEMI FATEMEH. Verification of Mobile Ad hoc Network Processes with Data. THE CSI JOURNAL ON COMPUTER SCIENCE AND ENGINEERING[Internet]. 2018;15(2):44-52. Available from: https://sid.ir/paper/775824/en

IEEE: Copy

FATEMEH GHASSEMI, “Verification of Mobile Ad hoc Network Processes with Data,” THE CSI JOURNAL ON COMPUTER SCIENCE AND ENGINEERING, vol. 15, no. 2, pp. 44–52, 2018, [Online]. Available: https://sid.ir/paper/775824/en

Related Journal Papers

No record.

Related Seminar Papers

No record.

Related Plans

No record.

Recommended Workshops