随着信息化技术的快速发展,软件系统作为信息基础设施,也随着需求的不断变化而变得更加庞大和复杂,其可靠性问题越来越受到人们的关注。软件参数配置差错,会导致重大的经济损失,在某些领域甚至会造成重大社会影响。以移动通信行业为例,新的组网模式、营销模式、业务种类层出不穷,要求不断修改和调整话单计费系统的资费配置参数,以适应需求的变化。资费配置差错会导致计费不正确,带来话费收入流失和客户投诉。现有计费正确性检测常常采用人工方式,存在覆盖性差、效率低下的问题。本文研究基于模型检查的移动话单计费正确性验证方法与实现技术。本文在剖析运行时计费系统的特性上,设计了特定的正确性验证系统,该验证系统由计费正确性验证和异常话单分析两部分组成。计费正确性验证是模拟现实场景自动生成测试话单的准确性检测模型,分为套餐模型、网络拓扑模型以及测试话单自动生成三个部分,其中套餐模型定义了话单计费的基本要素,网络拓扑描述了移动通信的网络拓扑结构,话单自动生成则描述了基于计费要素和网络拓扑结构生成测试话单的过程;异常话单分析主要针对由于计费基本要素缺失而被计费系统丢弃的这类异常话单进行统计分析。基于上述模型,分析了话单计费中的数据流特征,提出了基于模型检测的测试话单自动生成算法。该算法以现实中话单生成为基础,结合计费要素模型和相应的资费规则,采用虚拟拨测策略,生成符合需求的测试话单用例,达到验证计费系统中资费套餐参数配置是否正确的目的。最后,基于上述模型和算法,设计并实现了一个移动话单计费正确性验证系统,并在中国移动集团湖南公司正式投入使用。该系统对发现话单计费系统中存在的资费配置差错问题,提高移动公司计费正确性、提升客户满意度发挥了重要的作用。