Reliable Restricted Process Theory

Fatemeh Ghassemi, Wan Fokkink

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. To utilize our complete axiomatization for analyzing the correctness of protocols at the syntactic level, we introduce a precongruence relation which abstracts away from a sequence of multi-hop communications, leading to an application-level action preconditioned by a multi-hop constraint over the topology. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on our precongruence relation.

Original languageEnglish
Pages (from-to)1-41
Number of pages41
JournalFundamenta Informaticae
Volume165
Issue number1
DOIs
Publication statusPublished - 14 Feb 2019

Fingerprint

Communication
Network protocols
Network Protocols
Axiomatization
Multi-hop
Mobile ad hoc networks
Mobile Ad Hoc Networks
Correctness
Syntactics
Equivalence relation
Routing Protocol
Routing protocols
Broadcast
Semantics
Topology
Specification
Specifications
Vertex of a graph
Operator
Framework

Keywords

  • behavioral congruence
  • Mobile ad hoc network
  • process algebra
  • refinement
  • restricted broadcast

Cite this

Ghassemi, Fatemeh ; Fokkink, Wan. / Reliable Restricted Process Theory. In: Fundamenta Informaticae. 2019 ; Vol. 165, No. 1. pp. 1-41.
@article{7ce5d0f3de7544d3a48b5ab95886ef79,
title = "Reliable Restricted Process Theory",
abstract = "Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. To utilize our complete axiomatization for analyzing the correctness of protocols at the syntactic level, we introduce a precongruence relation which abstracts away from a sequence of multi-hop communications, leading to an application-level action preconditioned by a multi-hop constraint over the topology. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on our precongruence relation.",
keywords = "behavioral congruence, Mobile ad hoc network, process algebra, refinement, restricted broadcast",
author = "Fatemeh Ghassemi and Wan Fokkink",
year = "2019",
month = "2",
day = "14",
doi = "10.3233/FI-2019-1775",
language = "English",
volume = "165",
pages = "1--41",
journal = "Fundamenta Informaticae",
issn = "0169-2968",
publisher = "IOS Press",
number = "1",

}

Reliable Restricted Process Theory. / Ghassemi, Fatemeh; Fokkink, Wan.

In: Fundamenta Informaticae, Vol. 165, No. 1, 14.02.2019, p. 1-41.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Reliable Restricted Process Theory

AU - Ghassemi, Fatemeh

AU - Fokkink, Wan

PY - 2019/2/14

Y1 - 2019/2/14

N2 - Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. To utilize our complete axiomatization for analyzing the correctness of protocols at the syntactic level, we introduce a precongruence relation which abstracts away from a sequence of multi-hop communications, leading to an application-level action preconditioned by a multi-hop constraint over the topology. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on our precongruence relation.

AB - Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. To utilize our complete axiomatization for analyzing the correctness of protocols at the syntactic level, we introduce a precongruence relation which abstracts away from a sequence of multi-hop communications, leading to an application-level action preconditioned by a multi-hop constraint over the topology. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on our precongruence relation.

KW - behavioral congruence

KW - Mobile ad hoc network

KW - process algebra

KW - refinement

KW - restricted broadcast

UR - http://www.scopus.com/inward/record.url?scp=85062047723&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85062047723&partnerID=8YFLogxK

U2 - 10.3233/FI-2019-1775

DO - 10.3233/FI-2019-1775

M3 - Article

VL - 165

SP - 1

EP - 41

JO - Fundamenta Informaticae

JF - Fundamenta Informaticae

SN - 0169-2968

IS - 1

ER -