摘要：在现代公共交通体系中，轨道交通系统中的有轨电车具有重要地位。为了实现有轨电车安全、快速、高效地运行，科研人员不断的做出各种努力。随着计算机技术在列车运行控制系统中的应用，安全问题显得越发的重要和复杂，传统的安全系统设计、分析和测试方法难以满足以计算机技术为基础的安全系统的需要。近年来，基于离散数学和形式逻辑理论的形式化方法发展迅速，为解决安全计算机系统设计开发的正确性问题提供了一条可能的途径。
论文针对有轨电车的特点，研究安全系统设计的理论和方法，尝试采用形式化方法进行系统安全设计和验证。论文主要以有轨电车道岔控制和车载控制系统为研究对象，选择Cyber-Physical系统和AADL语言为系统形式化进行建模，提出时间自动机网络模型和相应的模型检验算法，进而给出形式化设计验证方法，且取得了不错的效果。
关键词：有轨电车；形式化方法；时间自动机
毕业设计说明书外文摘要
Title Research on Verification Method of Formal Development of Modern Tram
Abstract：In the modern public transport system， the tram in the rail transit system has an important position. In order to achieve the tram safe， fast and efficient operation， researchers continue to make all kinds of efforts. The vehicle control system and the turnout control system act as the nerve center of the tram to play the important task of guaranteeing the safety of driving and improving the running efficiency of the train. With the application of computer technology in the train operation control system， the security problem becomes more and more important and complicated. The traditional security system design， analysis and test method can not meet the needs of the computer technology based security system. In recent years， the formal method based on discrete mathematics and formal logic theory has developed rapidly， which provides a possible way to solve the correctness of the design and development of security computer system.
In view of the characteristics of tram， the paper studies the theory and method of safety system design， and tries to design and verify the system by using formal method. This paper mainly focuses on the trolley turnout control and vehicle control system， and chooses the Cyber-Physical system and AADL language to model the system formalization， and proposes the time automaton network model and the corresponding model checking algorithm， and then gives the formalization Design verification method， and achieved good results.
Keywords：Trams； formal methods； time automata
目次
1绪论.1
1.1研究背景.1
1.3研究目的及意义.2
1.4主要研究工作.3
2有轨电车信号系统方案研究.4
2.1有轨电车信号系统组成及其结构.4
2.2有轨电车信号系统的物理模型.5
3形式化建模方法.8
3.1形式化方法的发展与应用.8
3.2Cyber-PhysicalSystems技术.9
3.3混合架构分析与设计语言AADL.9
4有轨电车控制系统形式化建模11
4.1混合AADL的不确定性物理环境建模.11
4.2混合AADL建模设计示例.14
4.3不确定混合AADL模型的NPTA生成15
4.4从不确定混合AADL到NPTA的映射18
4.5后端配置与前端模型的生成18
4.6基于BLESS附件的PTA生成20
4.7基于混合附件的PTA生成21
4.8有轨电车系统模型22
结论.29
致谢.30
参考文献31
1 绪论
1.1 研究背景 现代有轨电车形式化开发验证方法研究:http://www.chuibin.com/zidonghua/lunwen_205404.html