Formalization of the Behavior of Content-Centric Networking
Formalization of the Behavior of Content-Centric Networking
复制标题
以内容为中心的网络行为的形式化
DOI：
10.1016/j.procs.2015.07.197
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Mizuki Goto and Kazuko Takahashi
中科院分区：
文献类型：
--
作者：
Sosuke Moriguchi;Takashi Morishima;Mizuki Goto and Kazuko Takahashi
内容中心网络（CCN）是一种基于内容名称而不是广告的通信架构。CCN中使用的协议不适用于端到端通信，而是适用于网络范围的通信。每个节点向连接到它的节点发送数据包，这些节点与连接到它们的其他节点通信。当数据被发送时，接收节点存储数据并将其转发给其他节点。这种数据存储提高了可靠性，并在服务器之间分配了负载;然而，协议的行为和性能需要进一步研究。在本文中，我们形式化的CCN协议使用证明助手Coq。这种形式化有两个方面：网络模块类型和协议的行为。网络模块类型具有若干参数，包括表示节点的数据类型、节点之间的连接关系以及取决于CCN的一些状态。在此基础上，给出了CCN中内容分发的两个规范的证明.通过基于模块类型的特定网络描述，我们直接获得了给定网络的这些规范的证明。该结果可用于增强CCN协议的可靠性。
Content-Centric Networking (CCN) is a communications architecture that is based on the names of contents, rather than on ad- dresses. The protocol used in CCN does not apply to end-to-end communications but is, instead, for network-wide communications. Each node sends packets to the nodes that are connected to it, which communicate with further nodes that are connected to them. When data are sent, the receiving nodes store the data and forward it to other nodes. Such data storage increases reliability and divides the load among servers; however, the behavior and performance of the protocol requires further investigation. In this paper, we formalize the CCN protocol using the proof assistant Coq. There are two aspects of this formalization: the network module type and the behavior of the protocol. The network module type has several parameters, including the data type denoting nodes, connection relations between nodes, and some status depending on the CCN. We then give proofs of two specifications for content- delivery in CCN. With a specific network description based on the module type, we obtain proofs of these specifications of the given network directly. This result can be used to enhance the reliability of CCN protocols.