B in Large-Scale Projects: The Canarsie Line CBTC Experience

B in Large-Scale Projects: The Canarsie Line CBTC Experience
复制标题

大型项目 B:Canarsie Line CBTC 体验

DOI:
--
复制
发表时间:
2007
期刊:
Formal Specification and Development in B
影响因子:
--
通讯作者:
Daniela Dolle
Daniela Dolle
中科院分区:
--
文献类型:
--
作者:
D. Essamé;Daniela Dolle

文献摘要

被引文献

相似文献

八年前,西门子交通系统公司在一个工业项目中首次成功应用了B方法。METEOR列车自动控制系统的关键软件采用B语言进行规范和编码,具有很强的可靠性和安全性要求。除了在工业环境中使用这种复杂的形式化方法的技术挑战之外,我们现在很清楚,使用B构建软件并不比使用传统方法更昂贵。更好的是,由于我们使用这种方法的经验,我们可以断言,在考虑整个开发过程(从规范到验证,有时是认证)时,使用B更便宜。自METEOR以来,西门子运输系统公司已经推广使用B来构建其系统的所有重要软件,特别是最近在纽约市Canarsie线上实施的基于通信的列车控制系统(CBTC)。这篇简短的论文分享了卡纳西线在B景观中的经验。
Eight years ago, Siemens Transportation Systems accomplished the first successful application of the B Method on an industrial project. The vital software of the METEOR automatic train control system, with very strong dependability and safety needs, was specified and coded in B. Beyond the technological challenge of using such a complex formal method in an industrial context, it is now clear for us that building software using B is not more expensive than using conventional methods. Better, due to our experience in using this method, we can assert that using B is cheaper when considering the whole development process (from specification to validation and sometimes certification). Since METEOR, Siemens Transportation Systems has generalized the use of B for building all vital software of its systems in particular its Communication Based Train Control Systems (CBTC) recently enacted on the New York City Canarsie Line. This short paper shares the Canarsie line experience in the B landscape.