混合選択とタイムアウトで拡張されたマルチパーティセッション型の軽量検査

• Item type: Trans(1)
• 公開日: 2021-06-15
• タイトル: 混合選択とタイムアウトで拡張されたマルチパーティセッション型の軽量検査
• タイトル / 言語: en
• タイトル: Lightweight Checking of Multiparty Session Types with Mixed Choice and Timeout
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要, Unrefereed Presentatin Abstract]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 岐阜大学
• 著者所属(英): en
• 著者所属(英): Gifu University
• 著者名: 今井, 敬吾
• 著者名(英): Keigo, Imai
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本発表は，混合選択（mixed choice）とタイムアウトによるマルチパーティセッション型（MPST）の拡張とその正しさを議論する．MPSTは，多者間の通信プログラムのデッドロックフリー性をプロトコルに基づく型付けにより保証する枠組みである．これまでの多くのセッション型では，外部選択（受信）と内部選択（送信）を通信プロトコルの1つの状態に混在させることはできず，表現力が低かった．混合選択により，受信メッセージが一定期間到達しなかった場合にタイムアウトを送信するといった振舞いを扱えるようになる．本手法は構文的で軽量な方法により混合選択を実現するので，モデル検査のような計算量の大きい外部ツールを必要としない点が新しく，また大きな特徴である．この軽量性を活かし，OCamlにおける通信ライブラリOCaml-MPSTの混合選択とタイムアウト拡張によるを示す．拡張の正しさの証明の方針として，型の構文的検査が従来の通信オートマトン（CFMS）におけるmultiparty compatibleの拡張されたクラスに相当することと，これがデッドロックフリー性を満たすことを議論する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Multiparty session types (MPST) are a type system that can ensure the safety of communication programs including deadlock-freedom. A mixed choice is a communication behaviour that mixes external choice (input) and internal choice (output) in a communication step, which is useful to handle various behaviours such as sending a timeout when a message is not received for a while. However, most MPST theories do not allow mixed choices, limiting the expressiveness of communication patterns. In this presentation, we discuss an extension of multiparty session types (MPST) with mixed choice and timeout, in a “syntactic” form, i.e. without resorting to state exploration like in model checking algorithms. To the author's knowledge, a syntactic checking of mixed choice is not investigated, Taking advantage of its lightweight form, we implement the mixed choice and timeout in OCaml-MPST, our communication library for OCaml. We discuss the new syntactic checking of MPST well-formedness corresponds to an extended class of multiparty compatible in communication automata (CFMS), which also guarantees deadlock-freedom.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 14, 号 3, p. 2-2, 発行日 2021-06-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会