作者：吴勇 李祥行为时序逻辑模型检测停止等待协议tlc
摘要：根据停止等待ARQ协议的算法,用基于TLA的系统描述语言TLA＋对ARQ协议进行建模,用TLC验证了ARQ协议应该满足的两条基本属性。根据ARQ协议的弱点在协议中加入一个攻击者行为Intuder,用TLC验证后,出现死锁造成ARQ拒绝服务攻击。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
《计算机安全》是一本有较高学术价值的月刊，自创刊以来，选题新奇而不失报道广度，服务大众而不失理论高度，颇受业界和广大读者的关注和好评。 《计算机安全》办刊方针：为网与计算机信息系统安全用户服务。更普及、更实用、更贴近读者。
部级期刊
人气 230965 评论 65
人气 216790 评论 35
省级期刊
人气 214071 评论 71
北大期刊、统计源期刊
人气 193654 评论 73
