CBTC中轨旁安全计算机的设计与形式化验证的中期报告CBTC系统是一种基于计算机的列车控制系统，用于提高地铁线路运行的安全性、效率和可靠性。中轨旁安全计算机是CBTC系统中的一个重要组成部分，负责监测列车和道路设备之间的通信，确保列车行驶安全。为了保证CBTC系统的可靠性和安全性，必须对中轨旁安全计算机进行形式化验证。本中期报告的目标是报告我们团队在设计和形式化验证CBTC中轨旁安全计算机方面取得的进展。在设计方面，我们根据CBTC系统的要求和需求，结合建模技术和设计方法，使用模型驱动工程的方法设计了中轨旁安全计算机，包括硬件和软件两个方面。我们还采用了符号执行方法对安全计算机软件进行了特性分析和代码审核，以确保软件的正确性和可靠性。在形式化验证方面，我们采用了基于模型的形式化验证方法，使用模型检查器对安全计算机的状态机模型进行了验证和分析。我们开发了状态机模型，描述了安全计算机的状态和转换规则，然后在模型检查器中对该模型进行了验证。通过模型检查器的分析，我们发现了一些潜在问题并及时进行了修正。目前，我们的工作已经完成了设计和形式化验证的大部分工作，还需进一步完善和检验。我们将继续完善安全计算机的设计和规格说明，进一步优化中轨旁安全计算机的性能和安全性，并将进行更全面的测试和验证。