Reliable restricted process theory

DOI10.3233/FI-2019-1775MaRDI QIDQ5377314zbMATH OpenFDO

Authors Fatemeh Ghassemi, Wan Fokkink

Publication date 24 May 2019

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1705.02600

zbMATH Keywords

behavioral congruencemobile ad hoc networkprocess algebrarefinementrestricted broadcast

Mathematics Subject Classification ID

Network protocols (68M12) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on a precongruence relation.

Recommendations

• Verification of mobile ad hoc networks: an algebraic approach
• Model checking mobile ad hoc networks
• A process calculus for mobile ad hoc networks
• A Calculus for Mobile Ad Hoc Networks
• An observational theory for mobile ad hoc networks (full version)

Cited in

(1)

• Formal methods for mobile ad hoc networks: a survey

This page was built for publication: Reliable restricted process theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5377314)