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

Specification and Verification of the Pastry Protocol Based on TLA

作　　者：刘照洋 龙士工[1] 

机构地区：[1]贵州大学计算机科学与技术学院,贵州贵阳550025

出　　处：《贵州大学学报（自然科学版）》2015年第6期79-82,87,共5页Journal of Guizhou University:Natural Sciences

基　　金：国家自然科学基金项目资助(61163001)

摘　　要：本文研究基于行为时序逻辑TLA的模型检测技术,阐述TLA的语义、语法和公平性问题。用基于TLA的系统描述语言TLA+对Pastry协议及其属性进行规约并用模型检测工具TLC对其进行验证。The Model checking based on Temporal Logic of Actions was researched, specifies the Syntax and Semantics of Temporal Logic of Actions were specified, the fairness of TLA briefly was defined, depicts PASTRY protocol and it＇s protocol with TLA ＋ based on the TLA and were depicted, and it was verified with TLC.

关 键 词：模型检测 PASTRY TLA TLC 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]