蓝牙是短距离、低成本无线通讯技术之一。它可以用于替代移动设备之间的通讯电缆,从而形成个人无线网络。它不仅使计算机和通信的融合成为可能,而且随着它的不断进步,还可以把家电、娱乐电子产品与计算机、通信系统的终端融为一体,使人们在家里、办公室或其他公共场所就能实现统一的操作和控制,为办公室的自动化和家庭通信的实施创造了良好的条件。蓝牙技术可视为开放的、全球无线语音和数据通信的技术标准之一。 蓝牙通信协议规范是由蓝牙特别利益组织制定的、全球开放的技术标准。它是设计蓝牙产品时所必须遵循的技术规范。本文在蓝牙技术规范的框架下,结合蓝牙协议的体系结构,重点分析了服务发现协议和逻辑链路控制和适配协议。并从协议分析出发,以协议分层的设计思想为理念,以协议工程学的方法为指导,充分利用有限状态自动机的工作方式,在LINUX平台上用ANSI C语言开发实现了这两个协议。 在对这两个协议开发实践的同时深入探索协议验证理论是本文的特点。在开发协议的过程中,本文将对网络协议的验证理论进行进一步的深层次研究。为解决复杂协议的验证问题以适应新的网络环境,在充分吸取当前的协议验证理论方法成果后,本文提出了一种新的网络协议的验证方法——基于多层自动机映射的网络协议的构建性的验证。文中不但对这一方法提供了严格的理论证明,而且给出了具体的验证步骤。