用于协议描述及验证的时态逻辑

A TEMPORAL LOGIC FOR THE SPECIFICATION AND VERIFICATION OF PROTOCOL

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

In this paper,we propose a now requirement based temporal logic tospecify and verify protocol.The sufficient and necessary condition that protocolpossesses safety and flexibility are presented.Temporal logic has many advantagessuch as strictness,directness,and convenience,In order to overcome deficiencies inapplying the logic to express history,a new operator(?)is difined.It simplifies thespecification and verification of protocol.The specification approach is illustratedwith examples of HDLC protocol.