铁路车站计算机联锁系统是运用“故障-安全”技术、计算机技术、网络技术以及容错技术等实现进路控制功能的系统。它不仅是实时系统,而且是安全-苛求系统。铁路车站计算机联锁软件是一种安全苛求软件,它在保障站内的行车安全、行车作业效率的提升等方面都起到及其关键的作用,是铁路车站计算机联锁系统的关键组成。目前,对联锁软件的设计阶段多采用自然语言,表现出很大的歧义性和二义性。本文基于面向对象理论,综合采用类图、用例图、协作图、序列图、状态图和活动图对联锁系统的进路控制过程及子过程进行建模。基于形式化方法,采用形式系统ALCQI-CTL,对模型进行形式化描述和说明,使模型的歧义性大大降低,减少主观因素差异造成的设计错误。论文针对车站联锁软件建模进行研究:(1)给出五元Kripke模型和语义,研究描述逻辑ALCQI,以及其语法和语义描述。基于形式系统ALCQI-CTL和形式系统ALCQI-CTL的序列图形式化方法,研究该系统的模型和形式化语义,并对该系统进行可行性分析。(2)建立系统的静态模型,研究计算机联锁系统的软硬件的组成和功能,以基本联锁原理为基础,采用用例图对计算机联锁软件的组成和功能进行描述,并采用类图设计信号机、道岔、轨道区段和进路的数据描述以及采用状态图设计对象的状态变化模型。(3)建立系统的动态模型,基于模块化思想,并且采用UML的一系列动态图建立一次进路控制过程的总体模型和过程的动态模型。建立一次进路控制过程和子过程的Kripke模型,基于形式系统ALCQI-CTL,并对其进行形式化描述和说明。(4)对模型进行实验,完成相关功能的验证工作。本文的研究结果表明:综合采用统一建模语言和形式化方法,能够高效地消除软件设计阶段由于人为因素差异造成的的缺陷和错误,使得计算机联锁领域专家和软件开发人员的联系更加紧密,提升联锁软件的安全性、可靠性;另一方面,能够在软件开发的初始阶段就及时发现软件设计中的缺陷和错误,同时,也减少了软件测试和验证的经济成本。验证结果表明:所建立的铁路车站计算机联锁软件的模型能充分应用于实际的需要。