论文部分内容阅读
采用模型检查技术,对IPv6的邻居发现协议的属性进行了形式化验证.该协议的模型由目前广泛用于设计和描述通信协议的MSC(message sequence charts)来描述,并通过线性时序逻辑说明该协议的属性.还提出了由MSC模型的线性化自动抽取协议属性的方法.
IPv6邻居发现协议的形式化验证
【摘 要】
：
采用模型检查技术,对IPv6的邻居发现协议的属性进行了形式化验证.该协议的模型由目前广泛用于设计和描述通信协议的MSC(message sequence charts)来描述,并通过线性时序逻辑
【机 构】
：
内蒙古大学,中国科学院
【出 处】
：
软件学报
【发表日期】
：
2005年6期
其他文献
现有的分布式实时协作系统多采用操作转换的方法来提供并发控制服务,但是在系统数据量很大时,系统性能不高.为解决这一问题,提出了一种新的并发控制方法madOPT:该方法利用对
Linux是目前广泛用于路由设备中的操作系统,而流量管理是这种网络操作系统的一个重要功能.研究了Linux系统的流量管理机制,发现当前Linux系统所采用的在网络接口的出口实现的
在给定的GC2插值条件,利用de Boor的构造平面曲线的GC2-Hermite插值方法,构造了一条具有两个自由度的三次B样条插值曲线,并证明插值曲线是局部存在的且具有4阶精度.
在广义粗集覆盖约简理论中,由于集合的上下近似是由其覆盖约简来确定的,因此有必要寻求一种新的度量来刻画知识和粗集的粗糙性.通过引入信息熵以刻画广义粗集覆盖约简的知识
职业技术教育是现代教育的重要组成部分，其发展的方向离不开教育的两大基本规律，即教育要适应社会发展的需要和教育要适应人的发展需要。职业技术教育要适应人的发展需要。职业
分析了王尚平等人提出的群签名成员删除方案,给出在群管理员更换群密钥后,已被删除成员更新其特性密钥、证明其成员资格和产生有效签名的方法,说明该方案是不安全的,不能真正