传感网是一种由具有感知、处理和无线通信能力的传感器节点通过自组织方式形成的一种多跳网络。随着传感网的迅速发展，传感网软件的规模逐渐变大，这使得不同的应用领域对传感网软件的性能都有着越来越高的要求。软件验证技术是保证软件性能的一项重要技术。模型检验是软件验证技术的一种，它为传感网软件验证提供了新的技术手段。在基于模型检验的软件验证领域中，状态空间爆炸问题是其发展的瓶颈。有界模型检验技术是模型检验领域新的研究方向，它通过限制建立模型时状态展开的次数来实现，主要用于缓解状态空间爆炸问题。本文主要对基于有界模型检验的传感网软件验证方法进行研究，该研究是面向源代码的，其实现主要分为两个工作：1）提出一种基于有界模型检验的传感网软件代码验证方法。该方法首先通过对传感网软件建立软件模型，实现对传感网软件的静态结构和动态行为的抽象；然后定义模型转换规则，将软件模型转化C语言代码；最后使用CBMC对转化后的代码进行有界模型检验。2）提出一种基于POR（偏序简约）的有界模型检验优化算法，该算法通过分段的方法来避免重复路径的搜索，较少状态遍历时间，