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

基于时间逻辑的通信协议形式化描述语言的研究

• 批准号: 60550243
• 负责人: ASANO Shoichiro
• 金额: $ 1.09万
• 依托单位: National Center for science Information System (1986-1987)The University of Tokyo (1985)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1985
• 资助国家: 日本
• 起止时间: 1985 至 1987
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-60550243/
• 关键词: 通信規約(プロトコル); 計算機言語; コンパイラ; 時間論理; 有限状態オートマトン; プロトコルの適合性検証; 検査系列

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.

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

项目成果

Shoichiro ASANO: Proceedings of INTERFACE Conference. INTERFACE85. CSC-3 (1985)

Shoichiro ASANO：INTERFACE 会议论文集。

Shoichiro ASANO et.al.: "Database Access Protocol for Chemical Information Network in Japan" Proceeding of ICCC'86. ICCC'86. (1986)

Shoichiro ASANO 等人：“日本化学信息网络数据库访问协议”ICCC86 论文集。

Shoichiro ASANO: 8th International Conference on Computer Communication. ICCC86. (1986)

Shoichiro ASANO：第八届国际计算机通信会议。

Shoichiro ASANO: Proceedings of Pacific Telecommunication Conference. PTC87. 531 (1987)

Shoichiro ASANO：太平洋电信会议记录。

Shoichiro ASANO: "Government,Supplier's and Use's Perspectives on Arriving at International Standards Agreements" proceedings of PTC'87. PTC'87. 531 (1987)

Shoichiro ASANO：“政府、供应商和用户对达成国际标准协议的看法”PTC87 会议记录。