ipv6邻居发现协议的形式化验证

采用模型检查技术,对ipv6的邻居发现协议的属性进行了形式化验证.该协议的模型由目前广泛用于设计和描述通信协议的msc(messagesequencecharts)来描述,并通过线性时序逻辑说明该协议的属性.还提出了由msc模型的线性化自动抽取协议属性的方法.