随着计算机越来越多的应用于安全苛求系统中,计算机能否长期安全、可靠、稳定的运行成为人们关注的中心,这促使着越来越多的人开始研究和设计安全计算机。而系统的安全性必须在设计阶段充分考虑,以免由于设计的缺陷导致整个系统存在安全隐患。所以在系统的设计过程中,根据安全苛求系统的“V”型的开发框架,采用形式化的方法对系统的安全性进行建模分析,验证系统设计的正确性和完备性是必要的。论文以基于通信的列车控制(CBTC)系统中ZC应用和DSU应用作为应用背景,以CBTC系统中ZC应用和DSU应用所使用的安全计算机平台为例。详细分析了安全计算机平台需求,在此基础上确定了系统结构,然后设计其硬件结构和软件的调度策略。论文引入有色Petri网,根据安全性设计思想,在系统的设计阶段对安全计算机平台进行形式化建模。首先介绍了有色Petri网的形式化层次化建模的方法,然后根据系统结构,采用“自上而下”的层次建模方法对系统建立的顶层模型和各级子模型,子模型包括“主”“备”通道模型、通道内单机模型、容错和安全管理单元(FTSM)模型和通信控制器模型。在所建模型的基础上,研究了CPN的状态空间分析和仿真性能分析两种方法在模型分析的应用。利用状态空间分析验证了容错和安全管理单元(FTSM)模块的有界性、活性等动态行为属性和逻辑功能的正确性;利用仿真分析完成了系统同步过程的性能分析,得出系统同步的时间参数,对系统调度时间的选取具有指导意义。通过对安全计算机进行建模和分析,可以验证对我们系统设计是否合理,对系统设计的完善提供参考和指导。