{"links":{},"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00211644","sets":["934:935:10452:10588"]},"path":["10588"],"owner":"44499","recid":"211644","title":["混合選択とタイムアウトで拡張されたマルチパーティセッション型の軽量検査"],"pubdate":{"attribute_name":"公開日","attribute_value":"2021-06-15"},"_buckets":{"deposit":"35f9ab66-96e5-4ce8-8640-a3cb4531e871"},"_deposit":{"id":"211644","pid":{"type":"depid","value":"211644","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"混合選択とタイムアウトで拡張されたマルチパーティセッション型の軽量検査","author_link":["538087","538086"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"混合選択とタイムアウトで拡張されたマルチパーティセッション型の軽量検査"},{"subitem_title":"Lightweight Checking of Multiparty Session Types with Mixed Choice and Timeout","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"[発表概要, Unrefereed Presentatin Abstract] ","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2021-06-15","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"岐阜大学"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Gifu University","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/211644/files/IPSJ-TPRO1403004.pdf","label":"IPSJ-TPRO1403004.pdf"},"date":[{"dateType":"Available","dateValue":"2023-06-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO1403004.pdf","filesize":[{"value":"92.4 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"5"},{"tax":["include_tax"],"price":"0","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"70766200-5fcd-465f-b2fe-aceb0d9902e0","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2021 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"今井, 敬吾"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Keigo, Imai","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"本発表は，混合選択（mixed choice）とタイムアウトによるマルチパーティセッション型（MPST）の拡張とその正しさを議論する．MPSTは，多者間の通信プログラムのデッドロックフリー性をプロトコルに基づく型付けにより保証する枠組みである．これまでの多くのセッション型では，外部選択（受信）と内部選択（送信）を通信プロトコルの1つの状態に混在させることはできず，表現力が低かった．混合選択により，受信メッセージが一定期間到達しなかった場合にタイムアウトを送信するといった振舞いを扱えるようになる．本手法は構文的で軽量な方法により混合選択を実現するので，モデル検査のような計算量の大きい外部ツールを必要としない点が新しく，また大きな特徴である．この軽量性を活かし，OCamlにおける通信ライブラリOCaml-MPSTの混合選択とタイムアウト拡張によるを示す．拡張の正しさの証明の方針として，型の構文的検査が従来の通信オートマトン（CFMS）におけるmultiparty compatibleの拡張されたクラスに相当することと，これがデッドロックフリー性を満たすことを議論する．","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"2","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicPageStart":"2","bibliographicIssueDates":{"bibliographicIssueDate":"2021-06-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"3","bibliographicVolumeNumber":"14"}]},"relation_version_is_last":true,"weko_creator_id":"44499"},"created":"2025-01-19T01:12:47.249377+00:00","updated":"2025-01-19T17:43:47.626632+00:00","id":211644}