A Study on Formal Description Language besed on Temporal logic for Communication Protocol

研究的目的是开发形式化描述的人工计算机语言来描述通信协议。最近，网络体系结构的框架，即OSI（开放系统互连），已经在国际上标准化了。OSI的概念一般适用于各种通信应用，在这些应用中需要定义复杂的通信协议。为了满足日益增长的应用需求，充分的通信协议表示是实现通信软件的重要因素。国际标准化组织（ISO）开始研究开发复杂协议的描述技术。本研究是在ISO研究的基础上进行的，ISO研究的目的是开发计算机可读语言和可执行语言。一种是基于PASCAL的“状态转换逻辑模型”语言的开发，另一种是基于“时态逻辑”语言的开发。在第一年和第二年的研究中，完成了这些方案的语言设计和协议表示能力的验证。去年讨论了编译器的设计，以实现所描述协议的直接执行。此外，还讨论了协议软件在一致性测试中的适用性。在这些讨论中，基于“时态逻辑”的描述语言被证明是协议形式化表示和协议软件描述的推荐语言。

The purpose of the research is to develop formal described artificial computer language to describe communication protocol. Recently,the framework for Metwork Architecture,that is OSI(Open System Interconnection),had been internationally standardized. The concept-of OSI is generally adapted to diversified applications on communication in where complicated communication protocols are defined.To meet with enhanced requirements on application,adaquate representation of communication protocols is of prime inportant factor to realize communication software. International Organization for Standardization (ISO) started researches to develop descriptio techniques for complex protocols. This research has been conducted with laison to ISO researches, where computer readable and executable languages are to be developed The research included two kind of development. One is the development of PASCAL based language with "State Transition Logical Model",and the other is of "Thmporal Logic" based language. In 1st and 2nd year of research,language design for these scheme,and verification of capabilities on protocol representation are finalized. In last year,compiler design is discussed to realize direct execution of described protocols. In addition to those,applicability to conformance & test for realized protocol software is also descussed.Throughout these discussion,"Temporal Logic" based description languge is demonstrated as a recommended language for formal representation of protocol and description of protocol software.