Tokeneer ID Station 规范的自动验证原型
软件工程
2020-09-03 v1
摘要
Tokeneer 项目由美国国家安全局（NSA）发起，旨在演示以具成本效益的方式应用严格方法开发高安全系统。Altran Praxis（英国）被 NSA 选中执行 Tokeneer ID Station 的开发。该公司编写了 Z 规范，随后以 SPARK Ada 编程语言实现，并使用 SPARK Examiner 工具集进行了验证。在本文中，我们展示 Z 规范可以轻松且自然地编码于 {log} 集合约束语言中，从而生成函数式原型。此外，我们展示 {log} 的自动证明能力能够解除所有关于状态不变量以及重要安全性质的证明义务。因此，该原型就所验证性质而言可被视为正确。这提供了经验证据：Z 用户可使用 {log} 从其 Z 规范生成正确原型。反过来，这些原型启用或简化了文中讨论的若干验证活动。
引用
@article{arxiv.2009.00999,
title = {An Automatically Verified Prototype of the Tokeneer ID Station Specification},
author = {Maximiliano Cristiá and Gianfranco Rossi},
journal= {arXiv preprint arXiv:2009.00999},
year = {2020}
}