论文部分内容阅读
本文提出了用一种新的基于要求时态逻辑对协议进行描述和验证,并给出了协议满足安全性和活性的充要条件。这种描述方法的优点在于严格、直观和方便。为了解决时态逻辑在表示过去时的不足,定义了新算子(?)表示历史,简化了协议的描述和验证。本文以HDLC为例,说明了协议的基于要求时态逻辑描述方法和协议的验证步骤及方法。