铁路车站联锁系统集成自动认证的安全性需求设计摘 要铁路联锁系统（RIS）是一个嵌入式系统（即一个监控系统），该系统是为了保证一个火车站的安全运行。当然，RIS是一个故障-安全系统。在本文中我们探讨在一个给定的行业系统即铁路联锁系统中设计集成自动形式化验证方法的可能性。我们的工作主要的障碍是：选择一个正式的验证工具，有效地解决手头的问题和设计验证的成本有效的整合策略等工具。最后，我们是能够设计出一个成功的整合策略以满足上述约束。而且这样做既不需要修改原设计也不用再培训人员。我们专为新加坡地铁的做了这项验证实验。实验表明，我们的集成策略自动验证系统设计的确能适应现实的生产实际。介 绍铁路联锁系统（RIS）是一个嵌入式系统（即一个监控系统），以确保在火车站的设备能安全运行。如RIS确保不可能使（无论手动或通过一些其他的系统自动控制）可能会导致列车碰撞的道岔发生动作。图1显示了一个联锁系统的作用在铁路控制层次。结构很明显，RIS是一个故障-安全系统。的确，RIS的客户（通常是铁路公司）越来越重视新设计的系统安全性的依据。权威机关和即将到来的标准（如CENEL
