通信系统的时态描述

本文建立一种描述通信系统外部行为的时态逻辑。该逻辑的基本谓词为INT,PASS和CLD,记录通信通道的瞬时状态,即打算通信,或正传递消息,或通道关闭。并引入辅助变元,将通道状态汇总为系统状态。从而使各类安全性、活性和公平性均能确切表述。使用这一逻辑进行描述时,还可得益于组合式规则——子描述的逻辑合取组成系统描述。本文还提出了证明由CSP语言书写的通信协议满足其行为描述的推理规则。