This paper is about the mechanical verification of UDP based network programs. It uses the UDP portion of a formal model of the internetprotocols TCP (Transmission Control protocol) and UDP (userdatagramprotocol). ...
详细信息
ISBN:
(纸本)1920682236
This paper is about the mechanical verification of UDP based network programs. It uses the UDP portion of a formal model of the internetprotocols TCP (Transmission Control protocol) and UDP (userdatagramprotocol). The model includes asynchronous message passing, message loss and host failure. The model is based around the sockets library, the primary API used for writing UDP and TCP based applications. This paper demonstrates that formal, machine-checked, proof is possible in the UDP model by presenting the proof of a safety property for an implementation of Stenning's protocol. The protocol is implemented in a fragment of the OCaml language, using the sockets library for UDP network communication. The entire development including the safety proof is carried out in the proof assistant Isabelle; this assures soundness. Thus this paper demonstrates that it is possible to machine verify very concrete representations of distributed programs in a detailed semantics that accurately reflects the programs execution environment. Previously only abstract representations of this protocol have been machine verified. The proof, based on an implementation, provides a contrast to other verifications.
The Constrained Application protocol (CoAP) is specifically designed for constrained IoT devices and is being rapidly deployed for the communication needs of the IoT devices. CoAP has been specified with its own conge...
详细信息
ISBN:
(纸本)9781538663592;9781538663585
The Constrained Application protocol (CoAP) is specifically designed for constrained IoT devices and is being rapidly deployed for the communication needs of the IoT devices. CoAP has been specified with its own congestion control algorithms because it runs on top of UDP that does not include any congestion control measures. These algorithms aim at taking into account the specific needs of the IoT communication. The need of running CoAP also over TCP has arised recently and is expected to be increasingly deployed alongside with CoAP over UDP. To understand the benefits and shortcomings of both CoAP over TCP and CoAP over UDP, we run an extensive set of experiments in different network settings and compare the performance of CoAP over TCP to the existing congestion control algorithms for CoAP over UDP. Our results reveal that even though CoAP over TCP has its known limitations it scales well and performs even better than expected in certain wireless settings that CoAP over UDP algorithms are specifically designed for, often even outperforming CoAP over UDP.
HTTP has been the protocol for transferring web traffic over the internet since the 90s. However, over the past 20 years websites have evolved so much that today this protocol does not provide optimal delivery over th...
详细信息
ISBN:
(纸本)9781479966653
HTTP has been the protocol for transferring web traffic over the internet since the 90s. However, over the past 20 years websites have evolved so much that today this protocol does not provide optimal delivery over the internet and became a bottleneck in decreasing page load times. Google is pioneering in finding better solutions for downloading web pages and they implemented two new protocols: SPDY in 2009 and QUIC in 2013. Since the wide range deployment of SPDY clients and servers it has been revealed that in some scenarios SPDY can negatively affect the page transfer time mainly due to the fact that the protocol is working over TCP. To tackle these obstacles QUIC uses its own congestion control and based on UDP in the transport layer. Since QUIC is a very recent protocol, this paper could help further understand its operation and performance in a wide range of network scenarios. We present a comprehensive study about the performance of QUIC, SPDY and HTTP particularly about how they affect page load time. We found that none of these protocols is clearly better than the other two and the actual network conditions determine which protocol performs the best.
Access Point (AP) selection is important in WLANs as it affects the throughput of the joining station (STA). In this paper, we propose a class of AP selection algorithms to maximize the joining STA's expected thro...
详细信息
ISBN:
(纸本)9781479959532
Access Point (AP) selection is important in WLANs as it affects the throughput of the joining station (STA). In this paper, we propose a class of AP selection algorithms to maximize the joining STA's expected throughput by considering interference at STAs, and transmit opportunities (TXOPs) at APs. Specifically, we collect a binary-valued local channel occupancy signal, called busy-idle (BI) signal, at each node and require the APs to periodically broadcast their BI signal and a quantity representing their TXOPs. This enables the joining STA to estimate throughput from candidate APs before selecting one. We use NS-2 simulations to demonstrate the effectiveness of our algorithms for saturated UDP and TCP downlink traffic, and compare them with received signal power (rxpwr) algorithm, load based algorithm, and Fukuda algorithm. For a random topology consisting of 24 APs and 60 STAs, our algorithms increase the joining STAs average throughput by as much as 42% and 24% compared to rxpwr for UDP and TCP respectively. The achieved average throughput is 90% and 93% of that obtained via the optimal selection. We also show that, in contrast to rxpwr, the throughput of proposed algorithms remains close to optimal with the increase in AP or STA density.
This paper addresses the development and implementation of a testbed for object's manipulation by using unmanned aerial vehicles *** and the VICON Cameras System. Such testbed allows the user to choose among two d...
详细信息
ISBN:
(纸本)9781479923779
This paper addresses the development and implementation of a testbed for object's manipulation by using unmanned aerial vehicles *** and the VICON Cameras System. Such testbed allows the user to choose among two development environments to perform aerial manipulation establishing a communication with LabVIEW, ROS and the C++ Qt library;thus, the user can employ the development environment more suitable for his application. This testbed allows us to establish communication between a computer and the A.R. Drone (v1 or v2) via a WiFi connection which sends and receives data using the communication protocol UDP and sockets for connection with the vehicle UDP ports. This platform sends control and navigation commands to the UAVs in order to position them in the space with user interaction by means of a graphical user interface. This testbed enables the implementation of more complex applications, such as complex controllers. In addition, to validate the effectiveness of this testbed, experimental results of aerial manipulation between two quadrotors are presented.
暂无评论