| 研究課題/領域番号 |
23K21654
|
|---|
| 補助金の研究課題番号 |
21H03415 (2021-2023)
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 基金 (2024)
補助金 (2021-2023) |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
|
|---|
| 研究分担者 |
小川 瑞史 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (40362024)
関 浩之 名古屋大学, 情報学研究科, 教授 (80196948)
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2024年度)
|
| 配分額 *注記 |
17,030千円 (直接経費: 13,100千円、間接経費: 3,930千円)
2025年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
2024年度: 3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2023年度: 3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2022年度: 2,600千円 (直接経費: 2,000千円、間接経費: 600千円)
2021年度: 3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
|
|---|
| キーワード | アクティブ学習 / 頑健性 / Assume-Gurantee検証 / 拡張有限状態オートマトン / 並行計算モデル / イベントクロックオートマトン / アクティブ学習アルゴリズム / 分割検証 / 到達可能性解析 / 時間付並行逆計算 / Assume-Gurantee / SMTソルバー |
|---|
| 研究開始時の研究の概要 |
実データを含むサブシステムの振舞いを拡張有限状態機械(EFSM)としてモデル化し振舞い合成と分解について、通信プロセスの形式化に基づい て振舞いの頑健性として振舞いの安定性を導く設計手法を確立する。この研究においては、システムの分解と合成の検証における抽象モデルと 実現モデルとの関係に着目して研究を行う。それぞれのサブシステム自体が持つサンプリングやクロックドリフトに基づく誤差が全体システム の安定性を損なわないことを保証する。合成、分解においては、全体の設計情報に基づいて相互に可能な振舞いを自動的に学習して、効率的で 現実的な検証およびテストのためのを設計モデルを導く。
|
| 研究実績の概要 |
本年度は，前年度に引き続いて、可逆計算を実現する実行環境の実現と時間経過モデルに対して可逆計算の概念を導入したモデルについて検討した．時間経過モデルは，複数のコンポーネントが同期をする際に通信を行わず，互いに持つクロックの差分によって同期を可能にする．離散的時間経過を並行的に可逆的に進行する計算をプロセス計算に基づいて定義し、イタリアの研究者と共同して雑誌論文に発表した。
可逆計算を並行計算モデルに適用した場合には，実行時の依存関係を記録して，不具合が発生したときにどの依存関係が設計時に想定した正しさに適合しないかをチェックすることができる．時間を導入した計算モデルの応用を実現するための基盤として中間言語による可逆実行環境を設計し，その可逆性を理論的に証明した．可逆実行におけるデータフロー解析手法を示し，効率的な可逆実行とフロー解析手法について論文発表を行った．可逆プログラミング言語への時間経過の導入とともに，通信プロセスの枠組みで新たな形式モデルについての論文発表ができた． 可逆計算モデルに基づく中間言語としてCRIL(Concurrent Riversible Intermediate Language)を提案し，その可逆意味論を提案した．可逆意味論は独立性をもつラベル遷移系として定式化でき，Laneseらの枠組みに基づいて可逆意味論として適当な振舞いをすることが示される．このプログラミング言語は，プログラミングに用いる高級言語と実行メカニズムの中間に位置する中間言語であり，コンパイラにおける解析言語としての位置づけを持つ．この枠組み対する時間経過による同期機構の導入の基盤とすることができるため，時間拡張のための基盤が構成できたと考えている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本年度は，可逆計算の概念を導入したモデルについてにおける実行向けのプログラミング言語CRILを提案した．このモデルでは並行システムが実行環境に応じて非決定的に動作することによって動的に変化する依存関係を計算の意味として保存する．可逆計算モデルを導入することによってより精密な解析が可能となる知見にもとづいてプログラムを可逆的に実行する具体的なメカニズムを提案し，並行実行において，因果安全性と因果活性を持つことを示した．
これらの性質によって，機械向きの中間言語に変換して上で実行すれば並行性に対する可逆性が保証させる．このことは，デバッグにおいてスレッド毎にできるだけ独立したデバッグを行い，必要に応じて因果関係を保存した実行が可能であることを示す．本年度得られた離散時間意味を導入して実行系を拡張すれば，実時間システムにおけるより詳細な解析やデバッグか可能となることの見通しが得られた．
さらに実時間性を持つプログラムの解析手法として，ゾーン解析による時間経過による振舞いの離散的モデル化による到達可能性解析について，シミュレーション関係に基づいた決定可能性について引き続き検討を行っている．入れ子構造を持つ計算モデル(Nested Timed Automata)を対象とし，ゾーンの領域に基づいた決定可能性について証明を与えるとともに，アクティブ学習への応用についての基本的な調査を継続する．
|
| 今後の研究の推進方策 |
今後は，可逆的計算を含めたアクティブ学習の枠組みについて重点をおいて研究をすすめる計画である．可逆計算に基づく実行意味は非常に有用であることから，誤差解析への応用を検討するとともに，アクティブ学習への応用手法について引き続き研究をすすめる．時間経過に関する振舞いにおけるタイマーについての対称性を導入するために，イベントクロックオートマトンでイベント予測クロックによる振舞いのアクティブ学習について研究する．イベント予測クロックは予測時点に遡って振舞いが決まることから逆計算によるモデル化によってイベント記録クロックと対象の学習メカニズムが適用できることが予想され，一定の仮定を新たに設定することでアクティブ学習を可能にする方法について研究を進める．イベント予測クロックは可逆通信プロセスにおいても重要な役割をすることが予測され，可逆通信プロセス計算の研究に対しても有用である．時間プッシュオートマトンの拡張体系であるNeTAについても凍結クロックを導入した到達可能性についても研究を進める．
|
