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
AN - SCOPUS:85062047723
SN - 0169-2968
VL - 165
SP - 1
EP - 41
JO - Fundamenta Informaticae
JF - Fundamenta Informaticae
IS - 1
ER -