随着安全苛求系统在铁路、航空航天、工业控制等领域应用得越来越广泛,安全计算机技术的发展越来越受到人们的重视,已经形成了一个专门的学术分支。为了扩大适用范围、减少开发成本和维护成本,安全计算机的开发正朝着通用化、可升级、可扩展等方向发展。本文以基于通信的列车运行控制系统(CBTC)中区域控制器(ZC)和数据存储单元(DSU)为应用背景,通过对采用硬件、软件冗余结合方式的可扩展安全计算机平台的设计,研究了基于模型工程的系统开发方法在安全计算机平台设计中的应用。论文引入了基于形式化方法的模型工程概念,在系统开发早期和整个开发生命周期内对系统进行建模和验证,以尽早发现设计中存在的问题。架构分析和设计语言(AADL)是一种支持模型工程的形式化建模语言。本文从基于AADL的系统开发生命周期模型出发,完成了对CBTC系统中的安全计算机平台的系统需求分析、系统高层AADL建模、平台软件AADL建模和验证。根据对CBTC系统安全计算机平台的需求分析,设计了安全计算机平台的高层AADL模型,并描述了该三模冗余安全计算机平台实际结构。该结构由应用软件、平台软件、处理器和专门的冗余管理硬件单元(RM)组成的。论文详细描述了安全计算机平台的工作原理和RM硬件单元的逻辑功能。论文详细介绍了平台软件流程,并根据该流程设计了基于AADL的平台软件详细AADL模型,包括系统表决、系统模式转化和系统重构等模块。根据列车运行控制系统的安全计算机平台的需求,利用工具软件OSATE验证了基于AADL的实时响应时间、系统安全等级和可调度性等特性,验证结果表明了系统的完备性和设计的合理性。可扩展安全计算机平台原理样机的制作和调试成功进一步证明了系统设计的正确性和可行性,也表明了以建模、验证为基础的模型工程开发方法适用于安全计算机平台的设计。