| 研究課題/領域番号 |
21K11822
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
渡部 卓雄 東京工業大学, 情報理工学院, 教授 (20222408)
|
|---|
| 研究分担者 |
森口 草介 東京工業大学, 情報理工学院, 助教 (60733409)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2023年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2022年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2021年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | 関数リアクティブプログラミング / 実時間処理 / 非同期実行 / 組込みシステム / 分散システム / 対話的処理系 / サイバーフィジカルシステム / アクターモデル / 非同期処理 / 型システム |
|---|
| 研究開始時の研究の概要 |
アクターモデルの考え方を取り入れた関数リアクティブプログラミング(FRP)言語の利用が，サイバーフィジカルシステム(CPS)の実行効率および信頼性の向上に寄与することを明らかにする．
本研究の特色は，非同期通信に基づく並行計算モデルであるアクターモデルを用いてFRP言語の実行系を実現することで，宣言的記述による高信頼CPSの開発支援と，非同期性による高効率な実行の両方を可能にすることにある．これにより，実時間処理や協調・耐故障動作等を副作用のない関数として表現することによる記述性向上と形式的検証の実現，および非同期実行や間欠実行による省電力化と高速化がそれぞれ可能になることを明らかにする．
|
| 研究実績の概要 |
(a) 小規模組込みシステム向け関数リアクティブプログラミング(FRP)言語のための実時間処理機構においての研究を行なった．まず，時変値に更新タイミングを明記するという形で周期的および非周期的な実時間離散イベントを表現する機構を導入したFRP言語EvEmfrpを設計・実装し，いくつかの具体例を用いた評価を通してその有効性を明らかにした．加えて，時系列に沿ったイベント系列をまとめて記述する機構（時間記述）を持つ言語TEFRPを提案した．
(b) 上記(a)で実装したEvEmfrpの実行系では周期的な間欠実行によって消費電力の削減を図っているが，非同期的に発生するイベントに対して実行周期の柔軟な制御ができないために消費電力の削減が十分に行われない．この問題への解決策として，非同期イベントを起点にして実行周期を動的に切り替える機構を持つ拡張言語EvEmfrp/Sを提案し，具体例を通して電力削減の機会が増加することを示すとともに，実機による評価を行い，提案の有用性を示した．
(c) FRPにおいては，グリッチ（時変値の更新タイミングによって値が異なってしまう現象）の発生は望ましくない．特に分散システムでは，グリッチ回避のための時変値更新順序の制御は大きなオーバーヘッドとなる．本研究では，システムを構成する時変値をパーティーと呼ばれるグループに分割し，パーティー内での時変値更新順序を制御することでグリッチを回避する手法を提案・実装し，その有効性を示した．
(d) マイクロコントローラの性能向上に伴う消費電力増加に対応して，低電力コプロセッサを導入したSoCが一般的になりつつあるが，そのプログラミングは複雑であり十分に活用されていない．我々は状態遷移記述を導入したFRP言語XStormを拡張してコプロセッサでの実行を容易にする機構を提案・実装し，その有効性を明らかにした．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究成果概要の(a)および(b)に述べた成果は関数リアクティブプログラミング(FRP)言語における実時間処理の記述方式とその効率的な実行方式の提案であり，本研究課題の目的であるCPS向けFRP言語の実行基盤となるべきものである．また昨年度に引き続き，提案した言語機構の組込みシステムにおける消費電力への影響に関する実験を行い，(b)においてより電力効率が向上していることを確認している．以上の点において，本研究はおおむね順調に進展している．
また，研究成果概要の(d)で示した通り，省電力コプロセッサをFRP言語において活用するという新たな研究課題に取り組み，その有効性を示すための実験を行うことができた．この点においても，予定していたFRP言語における実行時リソースの制御についての研究はおおむね順調に進展している．
加えて，同期計算モデルにおける逆計算についての研究を開始した．具体的には，同期計算モデルにもとづく計算系において，その出力から入力を再現することができる諸条件を明らかにしている．同期計算モデルはCPSの計算モデルとしても有用であり，その逆計算については，デバッグ（リバースデバッギング）への応用などが考えられる．この研究は当初の予定にはなかったが，高信頼CPSの構築つながるものであり，本研究課題の目的に沿っている．本年度末の時点でこの研究についての雑誌論文が投稿済みであり，その点でおおむね順調に進展している．
|
| 今後の研究の推進方策 |
当初の計画では本年度（2023年度）が最終年度であるが，期間を1年間延長し，次年度は以下(a)(b)を実施する．
(a) 現在，組込みシステムにおけるセンサ等の周辺機器の状態をFRPにおいてより適切に扱うことのできる言語機構を提案し，その有効性を示すための実装を行っている．具体的には，研究代表者・分担者の研究室で開発した，状態遷移モデルを内在した組込みシステム向けFRP言語XStormを拡張し，周辺機器の状態を安全かつ簡潔に扱う機能を追加している．これにより，様々な周辺機器の状態をFRPにおいてより安全に扱うことが可能となる．この実装を完成させ，評価を行う．
(b) 現在までの進捗状況の理由で述べた，同期計算システムにおける逆計算についての研究を引き続き行う．現在までに出力から入力を再現することのできる諸条件を明らかにしているが，その証明をより精密に行う．具体的には，本年度末の時点で進行中である，定理証明支援系Agdaを使った本研究の定式化および証明を完成させる．加えて，逆計算のデバッグ等への応用について検討する．
|
