メッセージ衝突を含む2プロセスのプロトコル仕様の自動合成

• Item type: SIG Technical Reports(1)
• 公開日: 1993-07-08
• タイトル: メッセージ衝突を含む2プロセスのプロトコル仕様の自動合成
• タイトル / 言語: en
• タイトル: Automated Synthesis of Two Process Protocol Specifications with Message Collisions
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 大阪大学基礎工学部情報工学科
• 著者所属: 大阪大学基礎工学部情報工学科
• 著者所属: 大阪大学基礎工学部情報工学科
• 著者所属: 大阪大学基礎工学部情報工学科
• 著者所属(英): en
• 著者所属(英): Dept. of Information and Computer Sciences Faculty of Engineering Science Osaka University
• 著者所属(英): en
• 著者所属(英): Dept. of Information and Computer Sciences Faculty of Engineering Science Osaka University
• 著者所属(英): en
• 著者所属(英): Dept. of Information and Computer Sciences Faculty of Engineering Science Osaka University
• 著者所属(英): en
• 著者所属(英): Dept. of Information and Computer Sciences Faculty of Engineering Science Osaka University
• 著者名: 五十嵐, 裕孝; 浅田, 宏幸; 角田, 良明; 菊野, 亨
• 著者名(英): Hirotaka, Igarashi; Hiroyuki, Asada; Yoshiaki, Kakuda; Tohru, Kikuno
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: プロトコル合成とは，サービス仕様からプロトコル仕様を導出することである．従来，提案された方法ではサービス仕様中に，異なったサービスアクセスポイントでプリミティブを上位層から下位層へ同時に送信する記述が含まれている場合，導出されるプロトコル仕様にメッセージ衝突による未定義受信が含まれるという欠点があった．また，従来の方法では，導出されたプロトコル仕様のいかなる遷移系列を実行するときの時間がリアルタイム通信のために指定されている上限値を越えるかを効率良く判定することができなかった．本論文ではまず，上述した性質を有するサービス仕様から2プロセスのプロトコル仕様を導出する自動合成法を提案する．この方法で合成されたプロトコル仕様には，メッセージ衝突に起因する未定義受信が含まれないと言った特徴がある．次に，その合成されたプロトコル仕様がリアルタイム性を満たしているかどうかを効率良く判定する方法を提案する．提案する検証法では，プロトコル仕様のなかの全ての遷移系列を多項式時間で導出する．このため，リアルタイム性の判定を効率良く行なうことができる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Protocol synthesis is to derive a protocol specification based on a service specification. In the previous methods, if the service specification includes simultaneous transmission of primitives from a high layer to a low layer through different service access points, then the derived protocol specification includes protocol errors of unspecified reception caused by message collisions. Furthermore, the previous protocol synthesis methods do not include efficient procedures to verify whether execution times along any acyclic sequence of transitions in the synthesized protocol specifications are no more than a specified bound for realtime communication. This paper proposes a method for automated synthesis of a protocol specification with two processes from a service specification described above. Protocol specifications derived from the service specifications by the proposed synthesis method are free from protocol errors of unspecified receptions due to message collisions. This paper also proposes an efficient verification method for determining a realtime bound in the synthesized protocol specification. In this method, all sequences of transitions in the protocol specification are enumerated in a polynomial time. This scheme enables the efficient verification of the realtime bound.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10444176
• 書誌情報: 情報処理学会研究報告システムソフトウェアとオペレーティング・システム（OS）; 巻 1993, 号 58(1993-OS-060), p. 123-130, 発行日 1993-07-08
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会