位置:成果数据库 > 期刊 > 期刊详情页
Formal Specification CSMA/CA Using Finite and Model-Checking of Precision Timed Automata
  • ISSN号:1005-8885
  • 期刊名称:《中国邮电高校学报:英文版》
  • 时间:0
  • 分类:TN925.93[电子电信—通信与信息系统;电子电信—信息与通信工程]
  • 作者机构:[1]Beijing University of Posts and Telecommunications, Beijing 100876, P.R. China, [2]Lab of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China
  • 相关基金:The work reported in this paper is supported by the National Grand Fundamental Research 973 Program of China (2002cb312200), and the National Natural SCience Foundation of China(60242002, 60273025).
中文摘要:

这篇论文论述正式说明并且有用我们为即时系统开发了的模型检查器的碰撞回避(CSMA/CA ) 协议的 CarrierSense 多重存取检查模型,当有限精确的网络预定了自动机,它被指定。CSMA/CA 协议在 IEEE 建议 802.11 标准被设计在无线随机的存取环境在传播期间减少碰撞的概率。然而,它不完全消除在二之间的碰撞或同时播送的更多的框架的可能性。我们调查什么将产生在框架之间的碰撞并且使用我们的自动确认工具为检查模型。

英文摘要:

This paper presents the formal specification and model-checklng of Carrier Sense Multiple Access with Collision Avoidance( CSMA/CA) protocol using the model checker we developed for real-time systems, which are specified as networks of finite precision timed automata. The CSMA/CA protocol proposed in the IEEE 802.11 standard is designed to reduce the probability of collision during a transmission in wireless random access environments. However, it does not eliminate completely the possibility of a collision between two or more frames transmitted simultaneously. We investigate what will give rise to a collision between frames and use our automatic verification tool for model-checking.

同期刊论文项目
同项目期刊论文
期刊信息
  • 《中国邮电高校学报:英文版》
  • 主管单位:高教部
  • 主办单位:北京邮电大学、南邮、重邮、西邮、长邮、石邮
  • 主编:LU Yinghua
  • 地址:北京231信箱(中国邮电大学)
  • 邮编:100704
  • 邮箱:jchupt@bupt.edu.cn
  • 电话:010-62282493
  • 国际标准刊号:ISSN:1005-8885
  • 国内统一刊号:ISSN:11-3486/TN
  • 邮发代号:2-629
  • 获奖情况:
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,波兰哥白尼索引,荷兰文摘与引文数据库,美国工程索引,美国剑桥科学文摘,英国科学文摘数据库
  • 被引量:127