Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA Process Algebra for Link Layer Protocols
62
0
0.0
(
0
)
Added by
Rob van Glabbeek
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling frame collisions. We also formalise suitable liveness properties for link layer protocols specified in this framework. To show applicability we model and analyse t
rate research
Read More
Routing protocol specifications are traditionally written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. Formal methods techniques, such as process algebras, avoid these problems, thus leading to more precise and verifiable descriptions of protocols. In this paper we use the timed process algebra T-AWN for modelling the Optimised Link State Routing protocol (OLSR) version 2.
Quantum computing holds a great promise and this work proposes to use new quantum data networks (QDNs) to connect multiple small quantum computers to form a cluster. Such a QDN differs from existing QKD networks in that the former must deliver data qubits reliably within itself. Two types of QDNs are studied, one using teleportation and the other using tell-and-go (TAG) to exchange quantum data. Two corresponding quantum transport protocols (QTPs), named Tele-QTP and TAG-QTP, are proposed to address many unique design challenges involved in reliable delivery of data qubits, and constraints imposed by quantum physics laws such as the no-cloning theorem, and limited availability of quantum memory. The proposed Tele-QTP and TAG-QTP are the first transport layer protocols for QDNs, complementing other works on the network protocol stack. Tele-QTP and TAG-QTP have novel mechanisms to support congestion-free and reliable delivery of streams of data qubits by managing the limited quantum memory at end hosts as well as intermediate nodes. Both analysis and extensive simulations show that the proposed QTPs can achieve a high throughput and fairness. This study also offers new insights into potential tradeoffs involved in using the two methods, teleportation and TAG, in two types of QDNs.
Network verification promises to detect errors, such as black holes and forwarding loops, by logically analyzing the control or data plane. To do so efficiently, the state-of-the-art (e.g., Veriflow) partitions packet headers with identical forwarding behavior into the same packet equivalence class (PEC). Recently, Yang and Lam showed how to construct the minimal set of PECs, called atomic predicates. Their construction uses Binary Decision Diagrams (BDDs). However, BDDs have been shown to incur significant overhead per packet header bit, performing poorly when analyzing large-scale data centers. The overhead of atomic predicates prompted ddNF to devise a specialized data structure of Ternary Bit Vectors (TBV) instead. However, TBVs are strictly less expressive than BDDs. Moreover, unlike atomic predicates, ddNFs set of PECs is not minimal. We show that ddNFs non-minimality is due to empty PECs. In addition, empty PECs are shown to trigger wrong analysis results. This reveals an inherent tension between precision, expressiveness and performance in formal network verification. Our paper resolves this tension through a new lattice-theoretical PEC-construction algorithm, #PEC, that advances the field as follows: (i) #PEC can encode more kinds of forwarding rules (e.g., ip-tables) than ddNF and Veriflow, (ii) #PEC verifies a wider class of errors (e.g., shadowed rules) than ddNF, and (iii) on a broad range of real-world datasets, #PEC is 10X faster than atomic predicates. By achieving precision, expressiveness and performance, this paper answers a longstanding quest that has spanned three generations of formal network analysis techniques.
We present a process algebra based approach to formalize the interactions of computing devices such as the representation of policies and the resolution of conflicts. As an example we specify how promises may be used in coming to an agreement regarding a simple though practical transportation problem.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
