時間制約を考慮した通信プロトコルの等価性検証アルゴリズムの開発に関する研究

1993 Fiscal Year Annual Research Report

• Project/Area Number: 05750346
• Research Institution: Osaka University
• Principal Investigator: 東野 輝夫 大阪大学, 基礎工学部, 助教授 (80173144)
• Keywords: 通信プロトコル / リアルタイムシステム / 検証 / 等価性 / LOTOS / プロセス代数

Research Abstract

一般に通信プロトコルの要求仕様には各処理(イベントと呼ぶ)の実行開始時間や終了時間,タイムアウトの発生時間等の“時間制約"が記述されている場合が多い.しかし,実現の際にはハードウェアや通信回線の性能等の制約から要求仕様に書かれた時間制約を変更したい場合がある.ところが,これらの時間制約を変更すると,要求仕様では実行可能であったイベント系列が実行可能になったり,逆に要求仕様では考慮していないイベント系列が実行不可能になる等もとの要求仕様との等価性が保証されなくなる場合がある.このため,時間制約を変更した場合に等価性(“双模倣等価性"と呼ばれる)が保証されるかどうかを判定出来ることが望ましい.本研究では,ISO(国際標準化機構)において通信プロトコルの形式記述言語として標準化されたLOTOSに時間制約を簡便に記述するための機能を付加した新しい言語LOTOS/Tを提案し,LOTOS/Tで書かれた2つの仕様の等価性を判定するアルゴリズムを考慮したる.取り扱う時間制約は,線形不等式の理論結合で記述できるクラスに限定し,線形計画法の手法を用いて等価性の判定を行っている.また,考慮した方法に基づいて等価性の判定を行う処理系を作成し,時間制約の異なる2つのリアルタイムシステムのLOTOS/T仕様の等価性を作成した処理系を用いて機械的に判定することにより,提案した手法の有効性を評価・検討した.これらの結果は,1993年10月に米国Bostonで行われたIFIP主催の第6回形式記述技法に関する国際会議(the 6th IFIP Int. Conf. on Formal Description Techniques)で発表した.

Research Products

• [Publications] A.Nakata: "LOTOS Enhancement to specify Time Constraints among Non-adjacent Actions using 1st-order Logic" Proc. of the sixth Int。Conf. on Formal Description Techniques (FORTE'93). 453-468 (1993)
• [Publications] 中田明夫: "時間制約付LOTOS記述の等価性の判定" 京都大学数理解析研究所講究録. (未定). (1994)
• [Publications] A.Nakata: "LOTOS Enhancement for Specifying Time Constraints Among Non-adjacent Actions and Verification of Equivalence" 情報処理学会研究報告. 93-DPS-61-19. 139-146 (1993)