| 研究課題/領域番号 |
24500033
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
渡部 卓雄 東京工業大学, 情報理工学(系)研究科, 准教授 (20222408)
|
|---|
| キーワード | 自己反映計算 / 広域自己反映計算 / アクターモデル / 文脈指向プログラミング / 並列文脈指向プログラミング / 実行時検証 |
|---|
| 研究概要 |
平成25年度は，前年度に引き続きある実行時検証に適したメタレベル計算の表現手法を含む自己反映的プログラムの構成方式の研究を行った．具体的には研究実施計画を踏襲し以下のようなタスクを実施した．
(1)広域自己反映計算の形式化とその検証方式：前年度に引き続き，アクターモデルをベースとした自己反映計算モデルの形式化およびその検証方式についての調査を行った．前年度の研究は個別のアクターにおける自己反映計算に限定されていたが，今年度は複数のアクターから構成されるグループを対象とする広域自己反映計算(GWR)に範囲を拡大した．具体的にはグループを構成するアクター群からそのグループと同等な振舞いを示す単一アクターの構成法を提案し，それにもとづいてGWRの定式化を行っている．この手法により，従来はアドホックに(ないしは実装依存な形で)定義されていたメタレベルを，個別のアクターのメタレベル定義から合成できること，および複数のアクターにまたがる自己反映的なふるまいを，合成後の単一のアクターの振る舞いとして定義できることを明らかにした．また，アクターモデルを用いて構成された系についての機械的検証を行うための準備として，Aπ計算(π計算に型による制約を導入してアクターモデルと同様にした体系)を定理証明支援系Coq上に実装し，その成果をGitHub上に公開している．
(2)並列文脈指向プログラミングの実現手法：上記(1)において得られた知見をもとに，並列システムにおける文脈指向プログラミング(COP)の実現手法を提案した．具体的には実行時文脈の変化をグループ内に非同期的に伝搬する手法をGWRを用いて定式化し，Erlang上に実現した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
現在までの成果は，研究実績の概要にあるようにほぼ研究実施計画に沿っている．広域自己反映計算を用いた並行文脈指向プログラミングの実現手法は研究計画時点ではなかったものであるが，前年度の実時間文脈指向プログラミングとあわせて本研究の適用範囲を拡大する上で重要である．また，Aπ計算を用いたアクターモデルの定式化をCoq上に実現できたことも特筆すべきである．以上より，現在までの達成度はおおむね順調であると判断できる．
|
| 今後の研究の推進方策 |
最終年度は，安全性に関する性質の記述形式およびその実行時検証手法についての研究(以下のタスク1~3)を行う． (1)ベースレベルにおける性質記述：ベースレベル(アプリケーション本来の動作レベル)の性質は，プログラムコード中の表明として記述する．一般にこの手法ではプログラムコード量が増大するにつれて表明の記述量が増大するという欠点がある．これに対しては，初年度に確立した証明の再利用方式を適用することで，この問題に対処する．
(2)メタレベルにおける性質記述：タスク(1)で述べたように，複数のアクターからなるグループのメタレベルは，そのグループを構成するアクターを合成することで構成できる．アクターモデルの操作的意味は遷移システムとして定式化されるが，合成してつくられたメタレベルアクターは単一のアクターであるため，その動作は非決定性を含む逐次計算として定式化される．よってメタレベルの振る舞いをLTLなどの時相論理を用いて記述する方法を確立する．
(B3)実行時検証機構のプロトタイプ実装：上で述べたように，メタオブジェクトは状態遷移系として表現され，その性質は時相論理式によって記述できる．正確には，ここで用いるのは過去時相論理と呼ばれるもので，現時点から過去にさかのぼった振る舞いについての性質を記述する．これは実行時検証に有効であり，我々の以前の研究においてもこの論理をベースとした記述を採用している．本研究でも過去時相 論理の一種であるPT-DTLを用いる．
|
| 次年度の研究費の使用計画 |
研究計画の軽微な改善によって効率的な予算執行が可能となり，結果として未使用額が発生した．具体的には，研究代表者自身が実験用プログラムを作成する時間がとれたことにより，プログラム作成補助のための謝金が不要となったこと，および消耗品として購入を予定していた開発用ソフトウェアをより効果的な代替品に置き換えることができたことによる．以上に加えて，各種機材のコストパフォーマンスの向上により，当初予定していたスペックの開発用器材がより安価に購入できたことが挙げられる．
最終年度は，アクターモデルを基礎とした広域自己反映計算にもとづく実行時検証機構のプロトタイプの実装および評価を行う．特に実時間組み込みシステム等を応用対象として評価を行うため，開発・実験用のパーソナルコンピュータに加え，実時間組み込みシステムのプロトタイプとして，センサや小規模ネットワークを備えたマイクロコンピュータボードを複数台必要とする．また，もう一つの応用であるwebアプリケーション等の分散システムを対象とする実験では，研究代表者の所属機関に設置されているスーパーコンピュータ(TSUBAME)を実験に用いる．よってそのための計算機使用料を必要とする．
上記の作業は研究代表者を入れて年度あたり約2人年程度の作業となる見積もりである．研究代表者以外の開発者(大学院生)についてはプログラム開発補助のための謝金を要する．また，研究上の情報交換のための旅費，および研究成果発表のための旅費を必要とする．
|
