认知无线电通信控制系统是面向山区无线通信应用系统的一个重要组成部分，包含数十个进程，一部分进程通过串口和网口与其他设备交互，一部分用于通信参数决策。各个进程间交互复杂，具有高度的并发性。而作为一个要在专门领域应用的系统，可靠性要求非常高，必须保证系统在各种条件下的正确性。基于形式化验证理论的模型检测技术是目前保证并发系统可靠性的有效途径之一。　　 本文基于形式化化验证的一般理论，分析了并发系统模型检测的技术特点，结合模型检测工具SPIN，探讨了用于解决状态爆炸问题的搜索优化技术。在此基础上，针对认知无线电通信控制系统的并发属性特点，基于SPIN工具，设计了分别在函数层、组件层、系统层等三个抽象层级上实施验证的方法。在函数层，对关键函数进行精确建模，实现验证模型与函数控制逻辑的一一对应;在组件层，对组件内各进程实行抽象建模，实现验证结果与组件接口设计的严格对应;在系统层，对系统内各个组件实行更高层次的抽象建模，实现验证结果与系统组件关系的一致对应。通过三层验证，分别在函数层和组件层发现了认知无线电通信控制系统软件的数个错误，进而，针对验证过程中发现的错误进行模型改进，通过反复迭代直到错误不再出现，保证了系统软件的可靠性。该验证结果在对实际系统的定向测试中得到了确认，表明本文所提出的无线电通信控制系统并发属性验证方法是可行的和有效的。