FTOS-Verify：容错系统非功能属性的分析与验证
分布式、并行与集群计算
2009-05-26 v1 计算机科学中的逻辑
摘要
工具FTOS的重点是通过提供包括容错机制在内的非功能方面的代码生成来减轻设计者的负担。在此背景下，一个关键方面是确保为用户系统模型选择的机制足以抵抗底层故障假设中指定的故障。本文提出了验证中的形式化方法来支持这一主张。我们首先将FTOS的精度提升到纯数学构造，并制定了确定性假设，这是作为类似Giotto系统（例如FTOS）的扩展以配备容错能力所必需的。我们证明，具有确定性假设的系统的局部属性将在用作验证模型的修改后的同步系统中得以保持。这使得能够使用硬件验证中已知的技术。在实现方面，我们开发了一个名为FTOS-Verify的原型工具，将其部署为FTOS的Eclipse插件，并进行了几个案例研究。
引用
@article{arxiv.0905.3946,
title = {FTOS-Verify: Analysis and Verification of Non-Functional Properties for Fault-Tolerant Systems},
author = {Chih-Hong Cheng and Christian Buckl and Javier Esparza and Alois Knoll},
journal= {arXiv preprint arXiv:0905.3946},
year = {2009}
}
备注
(bibliography update)