计算机联锁软件的Z规格说明  

Z specification of the computer interlocking software

作　　者：王铁江[1] 郦萌[1] 

机构地区：[1]同济大学计算机科学与工程系,上海200331

出　　处：《铁道学报》2003年第4期62-66,共5页Journal of the China Railway Society

基　　金：铁道部科技研究开发计划项目(2002X007)

摘　　要：计算机联锁软件是一种典型的安全关键软件,具有非常复杂的联锁控制逻辑和以失效安全为核心的安全需求。形式化其安全需求是一件十分必要,也是一件十分艰巨的任务。本文使用形式化规格说明语言———Z语言来描述其安全需求,生成形式化规格说明。形式化规格说明不仅有助于提高计算机联锁软件的质量,而且也有利于将来对它进行更严格的测试。The computer interlocking software is a kind of typical safetycritical software, which has very complicated interlocking control logic and safety requirements with the core of failsafe. The formalization of its safety requirements is a quite necessary and difficult task. With the use of formal specification languageZ language, its safety requirements are represented as a formal specification. The specification is useful and helpful not only for improving the quality of computer interlocking software, but also for implementing more strict software testing.

关 键 词：形式化规格说明 Z语言 安全需求 计算机联锁 铁路信号 

分 类 号：U284[交通运输工程—交通信息工程及控制]