| 研究課題/領域番号 |
21K11827
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 岐阜大学 |
|---|
研究代表者 |
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| 研究課題ステータス |
中途終了 (2023年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2024年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2023年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2022年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2021年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
|
|---|
| キーワード | 並行ソフトウェア / 通信プロトコル / セッション型 / 関数型プログラミング言語 / OCaml / モデル検査 / 並行プログラミング / 型システム / 分散プログラミング |
|---|
| 研究開始時の研究の概要 |
プログラミング言語の「型」は，整数や文字列などの「データ」を分類し間違いを事前に検出するための仕組みです．これに類似する枠組みとして，例えばインターネットで用いられる通信ポートは，HTTP や SMTP といった通信プロトコルで分類されています．セッション型はこの「通信ポート」のプロトコルを表す「型」であり，プログラムにおけるデッドロックや競合条件などの通信記述の誤りを事前に検出できます．
本研究は，セッション型をプログラミング言語において活用する軽量な方法を理論と実装の両面で開発します．これにより，多くの人が高信頼な並行分散ソフトウェアを手軽に構築できるようになることを目指します．
|
| 研究実績の概要 |
研究実績は大まかに次の3つに分けられる．
(1) セッション型，プログラミング言語の型システムとモデル検査の統合．具体的には，従来の，ソフトウェア全体の通信プロトコル設計とその安全性の検証が必要な「トップダウン型」の開発手法ではなく，それらが不要な「ボトムアップ」の手法を確立し，その実装であるkmclibを実装した．その成果に関する論文は， トップレベル会議の1つである TACAS 2022 に採択された．
(2) セッション型の表現能力に関する探究．(2-1) マルチパーティセッション型の混合選択に関する理論的な検討を行った．混合選択は，通信プロトコル参加者が特定の状態において送信と受信の双方を選択できる機能であるが，これは実用的に重要である一方でデッドロックフリー性などの信頼性に関する理論的な基礎は未整備である．本研究課題では，その無限のトレースを扱うための理論的基礎を検討した．(2-2) マルチパーティセッション型のプロトコルを文脈自由文法へと拡張し，処理系Session C#に実装した．
(3) これらからの派生的な研究．(3-1) 上述(1)の派生として，プログラミング言語OCamlのアドホック多相に関する拡張を設計し実装した．アドホック多相は単一の関数名に対して，引数型に応じた複数の定義本体を与える多重定義の機能である．これにより，OCamlプログラムにおいて型ベースのディスパッチが可能となり，プログラミングの効率向上が期待できる．(3-2) 上述(2-1)の派生として，高階項書換えシステムの活用を検討した．この際，共同研究者である群馬大学浜名准教授の高階項書換えシステムの処理系SOLの改修に関与した．停止性判定ツールのコンペティションTermComp2022に参加し，入賞した．
また，上記(2),(3-1)の進行中の内容や成果を国内ワークショップ・研究会にて発表した．
|
