应答器系统作为实现地-车信息传输的重要设备，其向车载传输的报文数据的正确性直接关系到列车运行安全。应答器报文是由编制人员依据应答器应用原则将线路工程数据进行编制而得。然而应用原则只是从列控系统功能需求的角度定义了应答器的设置原则以及报文结构，并未具体描述如何编制报文;此外，基于文本语言描述的应用原则易产生二义性问题，简单地将应用原则转换为相关软件代码存在很大隐患。　　本论文针对上述问题，首先基于应用原则的要求，结合专家经验，提取出一套具体完备的报文编制规则，之后，针对编制规则的特点，提出一种对其建模验证的方法框架，其主要特点是能够在编制规则、模型、验证过程以及模型检验结果之间建立一条双向跟踪链。通过分析模型检验结果，不断迭代规则模型，最终得到满足质量要求的报文编制规则及对应模型，可用于指导报文编制以及相关工具的开发，这对确保报文数据的正确性有重要意义，且为后续应答器报文相关技术规范的修订提供支持。　　本文基于以上述过程，具体做了以下三个方面的工作:　　(1)从数据生命周期和数据结构的角度分析了应答器报文数据，总结了报文数据从生成、使用、归档到过时的全过程;构建了工程数据和报文数据的结构模型。之后深入挖掘分析应答器应用原则的内容要求，并总结分析了相关的专家经验，作为后续编制规则建模验证的基础。　　(2)以应答器应用原则等相关规范文档和专家经验为输入，提取出报文编制规则的整体框架，以具体类型的应答器对应的报文生成场景为例，对编制规则进行建模验证。首先对规则进行非形式化分析，输出规则管理报表以实现规则到模型的正向追踪;采用基于UML-NuSMV相结合的建模验证方法，建立报文编制规则的UML模型，之后将其用NuSMV形式化语言描述，输入模型检验工具进行验证，分析验证结果，不断修改、重新验证反例中的错误直至验证结果全部为真，最终得到满足质量要求的编制规则及对应模型。　　(3)基于编制规则和对应模型，开发自动化报文编制工具。以已开通的实际线路数据为例编制应答器报文，将工具生成的报文与线上使用的正确报文数据进行对比，证明了工具的正确性，且对比结果表明基于编制规则开发的报文编制工具提高了报文编制的自动化程度，再次表明规则模型的正确性和完整性，有助于确保报文数据的正确性，对保障列控系统安全运行有重要意义。