摘要：在现在的铁路信号设备维护工作中，微机监测是不可或缺的一种重要方法。铁路信号微机监测系统通过采集机实时监测信号设备的工作状态，并将监测数据发送给监测站机进行分析处理，这极大地方便了车站对各信号设备的管理和维护，同时也提高了铁路的安全度。本文对铁路信号微机监测系统中站机和采集机的通信过程进行分析，使用UPPAAL对该通信过程进行时间自动机建模，并为该通信系统模型的主要功能提出形式化验证语句进行验证。这些成果使得抽象的信号微机监测系统通信过程变得形象，对以后着眼于铁路信号微机监测系统通信的研究具有一定的理论价值和实践意义。80861

毕业论文关键词：铁路信号；微机监测；UPPAAL；形式化方法

Simulation of Communication Process of Railway Signal Microcomputer Monitoring System

Abstract：Microcomputer monitoring system is an essential means in current railway signal equipment maintenance work。 Microcomputer monitoring system can monitor the working status of signal equipment in real time through the acquisition machine and send the Monitored data to the monitor to analysis and processing, which greatly facilitates the station to the signal equipment management and maintenance, but also improve the safety of the railway。 In this paper, the communication process of station and acquisition machine in railway signal microcomputer monitoring system has been analyzed, and UPPAAL has been used to model the communication process automatically and the formal verification of the main function of the has been presented。 These works make the abstract communication process of signal computer monitoring system more concrete, which has a certain theoretical value and practical significance of the research of railway signal computer monitoring system communication in the future。

KeyWords: railway signal; microcomputer monitoring; UPPAAL; formal method

目  录

1  绪论 1

1。1  课题的研究背景 1

1。2  微机监测系统的发展和现状 1

1。3  本文研究内容及篇章结构安排 2

1。3。1  研究内容  2

1。3。2  文章组织结构2

2  微机监测系统通信过程分析 3

2。1  信号微机监测系统的结构3

2。2  采集机与站机通信需要的数据帧类型 4

2。3  通信过程分析 5

3  基于时间自动机的微机监测系统通信过程建模 7

3。1  形式化方法 7

3。1。1  形式化方法概述  7

3。1。2  形式化验证  7

3。2  时间自动机 8

3。3  实时系统验证软件UPPAAL  9

3。3。1  UPPAAL简介  9

3。3。2  UPPAAL中模型的基本组成 10

3。3。3  UPPAAL的规范验证语法  11

3。4 微机监测系统通信过程建模  11

3。4。1 微机监测系统站机建模   13

3。4。2 微机监测系统采集机建模  15

3。4。3 随机数据丢失模型  18

4  信号微机监测系统通信过程的仿真与验证  19

4。1 微机监测系统通信过程仿真  19

4。2 通信模型形式化验证  34

5  总结与展望  38

5。1 总结  38

5。2 展望  38

致谢   39

参考文献   40