随机模型检测是一种不仅可以分析系统的定性属性，而且还能用来对系统属性进行定量分析的高度自动化形式化技术，其基本思想是构造捕获系统行为的数学模型，然后用它来分析指定的定量属性。本文首先应用随机模型检测技术对射频识别（RFID）中的S-ALOHA协议和服务于人体无线局域网的IEEE802.15.6协议进行验证与定量分析，其次针对验证与分析过程中出现的空间爆炸问题，提出一种空间约简技术:连续随机逻辑的限界检测算法。论文的主要工作如下:　　1.论文首先依据RFID中S-ALOHA协议的工作原理及特性，将其动态行为抽象成能支持非确定性，离散时间以及概率选择的马尔科夫决策过程，然后利用随机模型检测技术验证标签能否完成数据的可靠性传输，实验结果表明标签最终完成数据传输的概率为1，这就说明随着标签数的增加，该协议都能够完成数据的传输。进一步在模型上计算数据成功发送的概率以及在退避计数器到达最大退避数时的概率，并与纯ALOHA协议做了对比，结果表明S-ALOHA发生冲突的概率比ALOHA要小得多，因此S-ALOHA因冲突发生而进入等待的情况明显减少，标签能够更快速的传输数据。最后计算出在不同最大退避数下标签发送数据的最大期望时间以及完成数据传输所需要的最长时间，结果表明随着最大退避数的增加，S-ALOHA的期望时间比ALOHA的小6个时间单位，同时也表明S-ALOHA发送数据的平均速度比ALOHA快1.2倍左右。　　2.IEEE802.15.6协议标准化是用来解决人体穿戴式传感器、植入装置等节点的数据传输。首先根据802.15.6协议中MAC层中CSMA/CA算法的随机等待等特性，把802.15.6协议建立为含概率选择、随机性与实时性的概率时间自动机模型。然后用随机模型检测技术对模型的可靠性进行验证，实验结果说明随着节点数目和数据包大小的增加，节点成功发送数据的概率逐渐下降，当有10个节点，数据包大小125个字节时，最终节点能完成数据传输的概率有0.57。节点传输数据失败既然无法避免，所以在创建人体无线局域网设置适当的节点数和数据包大小是提升协议服务质量的关键。最后计算了节点发送数据的期望时间，并与ZigBee做了对比。结果表明:IEEE802.15.6中的节点发送数据相比ZigBee有更少的期望时间，其发送数据的平均速度约是ZigBee的4倍。　　3.对上述两个协议的分析与验证的过程中，我们发现无论是S-ALOHA协议中bcmax和标签数的增加，还是802.15.6协议中节点数和数据包大小的增多都会导致空间状态数急剧的增长，为此本文提出一种连续随机逻辑(CSL)的限界模型检测算法来缓解状态空间爆炸问题。首先定义了并证明了CSL的限界语义;其次对转移概率的计算是全局空间上有效实现连续随机逻辑模型检测的关键技术，提出在路径长度的约束下转移概率的计算;最后对不同的算子提出相应的基于转移概率计算的限界检测算法。实验结果说明在可达深度较小的局部空间上可以完成属性的验证，则限界检测无论是在时间还是空间消耗上都优于全局检测算法。