2021 Fiscal Year Annual Research Report
Embedded Systems Development Support with the Integration of the Actor-Model and Functional Reactive Programming
| Project/Area Number |
18K11236
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
渡部 卓雄 東京工業大学, 情報理工学院, 教授 (20222408)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | 関数リアクティブプログラミング / 組込みシステム / 型システム / プログラミング言語 |
|---|
| Outline of Annual Research Achievements |
小規模組込みシステム向け関数リアクティブプログラミング(FRP)言語Emfrpに，データ構造の大きさを静的に規定するための型システムを導入し，その有用性を明らかにした．
Emfrpでは，プログラム実行時のメモリ使用量は静的に決定され，かつ時変値の更新処理の停止性が保証されている．したがってEmfrpのプログラムは実行時のメモリエラーやハングアップを起こさない．これらは実行時システムによる動的な検査を介さずに保証されるため，マイクロコントローラなどで構成された小規模組込みシステム向けソフトウェアを構築する上で望ましい性質である．しかしこれらの性質を満たすために，Emfrpでは関数やデータ型における再帰が禁止されていることに加え，繰り返しに相当する機構が導入されていない．そのため，リストや木のような再帰的かつしばしば動的に構築されるデータ構造とそれらを用いるアルゴリズムの自然な表現が難しい．これらは小規模組込みシステムにおいても有用であるが，Emfrpで同等のものを表現しようとすると煩雑な書き方を強いられることがある．
この問題を解決するために，データの大きさを扱うことのできる型システムBounded Construction Types (BCT)を提案し，それをEmfrpに導入することで再帰的データ構造とそれらを扱う再帰的関数を利用できるようにした．BCTは構築子（コンストラクタ）の総数を明記できるような代数的データ型である．これを用いることで，リストや木のような再帰的データ構造についてもそれらのサイズを静的に規定でき，またそれらを扱う再帰的関数についても停止性を保証できる．本研究ではBCTによって型付けされたプログラムはその実行時メモリ使用量が静的に確定されることを証明したのち，BCTを導入した拡張Emfrpのプロトタイプ処理系を実装し，例題を通してその有用性を示した．
|
