Parameterized Verification of Ad Hoc Networks
Parameterized Verification of Ad Hoc Networks
复制标题
Ad Hoc网络的参数化验证
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
G. Zavattaro
中科院分区：
文献类型：
--
作者：
G. Delzanno;Arnaud Sangnier;G. Zavattaro
我们研究了具有选择性广播和自发运动的临时网络形式模型的参数化验证的决策问题。网络的通信拓扑表示为图。节点代表单个过程的状态。相邻的节点代表单跳邻居。流程是有限状态自动机，通过选择性广播消息进行通信。广播的接待仅限于单跳邻居。对于此模型，我们考虑可以用一个节点（分别为所有节点）在特定状态下以任意数量的节点和未知拓扑的初始配置来表示的验证问题。根据通信图的不同假设，即静态，移动和有限的路径拓扑，我们绘制了这些问题的可确定性边界的完整图片。
We study decision problems for parameterized verification of a formal model of Ad Hoc Networks with selective broadcast and spontaneous movement. The communication topology of a network is represented as a graph. Nodes represent states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via selective broadcast messages. Reception of a broadcast is restricted to single-hop neighbors. For this model we consider verification problems that can be expressed as reachability of configurations with one node (resp. all nodes) in a certain state from an initial configuration with an arbitrary number of nodes and unknown topology. We draw a complete picture of the decidability boundaries of these problems according to different assumptions on communication graphs, namely static, mobile, and bounded path topology.