Abstract
本文提出一種描述通信協定的方法。用述句來表示一個分散系統的整體狀態，並用公理來描述這些狀態的轉變，可以得到一個明確的描述，並可用定理證明器加以分。定理證明可產生此系統所有可達到的狀態。利用此種分析，可以檢查出死結，迴圈或停滯完整性及此系統是否正確的結果。我們展示了用公理來定義通信協定的狀態變化，以描述通信協定行為的一個方法，並可用定理證明器來做可達狀態的產生器，這是一個相當一般化的方法。近來，測試中心的發展漸被重視，也有其他的方法試圖把效率也列入驗證通信協定正確性的因素之一。我們可說：軟體工程已擴展至包含分散處理的影響，在分散處理中出現旳許多問題，將隨這門工程的發展而找到解答。