Electronic Communications of the EASST Volume 46 ( 2011 ) Proceedings of the 11 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2011 ) Experiences in the Industrial use of Formal Methods
Electronic Communications of the EASST Volume 46 ( 2011 ) Proceedings of the 11 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2011 ) Experiences in the Industrial use of Formal Methods
复制标题
EASST 电子通信第 46 卷 (2011) 第 11 届关键系统自动验证国际研讨会论文集 (AVoCS 2011) 形式化方法的工业应用经验
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Janet Barnes
中科院分区：
文献类型：
--
作者：
Janet Barnes
Altran Praxis多年来一直在其高度完整的开发方法中使用形式化方法，即构造正确性（Correctness by Construction，CbyC）。为美国国家安全局（NSA）开发的令牌ID站（TIS）是使用正式方法和CbyC方法开发的一个例子。该项目使用了一些严格的技术，包括规范的形式化，使用Z符号，规范的细化到正式的设计，软件开发SPARK与软件的运行时错误的情况下的证明和系统属性的证明。自2008年向更广泛的社区开放以来，该项目经受住了严格的审查，只发现了五个错误。尽管该方法总体上取得了成功，但在工业环境中使用正式方法仍面临挑战。通过研究一些影响工业中工具和技术成功部署的关键属性，我们试图将正式方法的工业部署的挑战纳入视野。
Altran Praxis has used formal methods within its high integrity development approach, Correctness by Construction (CbyC), for a number of years. The Tokeneer ID Station (TIS) developed for the US National Security Agency (NSA) is one example of a development using formal methods and the CbyC approach. This project used a number of rigorous techniques including formalisation of the specification using the Z Notation, refinement of the specification to a formal design, software development in SPARK with proof of absence of run-time errors of the software and proof of system properties. The project has stood up well to the intense scrutiny it has been subject to since it became available to the wider community in 2008, with only five errors being found. Despite the general success of the approach there are challenges to using formal methods in an industrial context. By looking at a number of key properties that affect the success of deployment of tools and techniques in industry we attempt to put the challenges of industrial deployment of formal methods into perspective.