然后按照需求分析，进行各进路的建模，并将模型进行仿真模拟，通过反复模拟仿真，首先将比较明显的错误修正，然后不断完善模型，以致完成最终模型。
总之，论文利用时间自动机模型的UPPAAL软件，对办理进路的进路控制流程进行分析和建模，利用这种安全性设计方法对系统设计中存在问题予以纠正，使其更完善。取得了不错的效果。
但是由于论文的研究条件和时间限制，本文建立的形式化模型还不够完善，对课题的研究还需要进一步的一些工作。
由于联锁软件的逻辑十分复杂，本论文只研究了它的核心进路控制功能，还有的地方进行了一定的简化，这些都是在实际的应用设计和开发中需要考虑的。下一步还需要从整个系统需求的角度出发，逐步完善形式化模型。对于铁路中联锁的特点和一些特殊功能还可以进一步挖掘，比如列车运行的追踪进路、侧面防护等，这些都是铁路联锁需要重点关注的。
计算机联锁对于安全性和可靠性要求非常高，本论文的时间自动机的形式化建模和验证方法目前还停留在理论阶段，需要对建模方法和验证作深入的研究。有了形式化模型，如何将模型不断精化并且最终实现系统的形式化开发也是下一步研究的重点。 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(22):http://www.751com.cn/shuxue/lunwen_767.html