采用形式化验证是确认计算机联锁软件能够满足特定安全属性的一种有效手段。本文描述了一种基于模型检验的方法,对联锁系统模型及安全属性模型的建立方法进行探讨,并结合具体的站场实例,对信号开放功能进行了模型描述和验证,结果表明该方法用于计算机联锁系统具备可行性。