基于行为时序逻辑TLA的Pastry协议的规约与验证

本文研究基于行为时序逻辑TLA的模型检测技术,阐述TLA的语义、语法和公平性问题。用基于TLA的系统描述语言TLA+对Pastry协议及其属性进行规约并用模型检测工具TLC对其进行验证。