| 研究課題/領域番号 |
24700028
|
|---|
| 研究種目 |
若手研究(B)
|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2015-03-31
|
| キーワード | 分散プロセス計算 / プログラミング言語 / コード移動 / プログラム解析・検証 |
|---|
| 研究概要 |
平成24年度には，主に以下の2つの研究開発を行った.
(1) 高水準言語向けライブラリの仕様策定およびプロトタイプ実装：分散プログラムの柔軟な開発を目的とした，Scheme言語用ライブラリの開発を行った．開発した実行環境は，対話環境を備え，プログラムを実行させながら，アドホックなコードの追加，移動，マージ等のアンビエントの構造的な変更を柔軟に行うことが可能である．開発したライブラリは，移動を実現するための実装方式の提案，アンビエント階層可視化ツールの開発，関数型言語の持つ高階関数，スコープルールとの兼ね合いを考慮した仕様の設計等，高水準言語上でアンビエント計算モデルを用いてプログラムを記述するのに有用な機構を数多く備えている．
(2) 高水準言語向けライブラリの分散環境上における安全な実装技術の開発：アンビエントにおいて個々の移動動作を表すケーパビリティは，秘匿性と不可分性の2つの性質を備えている．秘匿性とはケーパビリティから動作対象の名前を抽出できないこと，不可分性とは，合成されたケーパビリティを個々の要素に分解できないことを意味する．これらの性質により，アンビエント間のやり取りに厳密な制限を課すことが出来，システムの安全性を保証しやすくなる．アンビエント計算の実装において，これら2つの性質を備えたケーパビリティを実現するための手法について提案する．提案手法は，公開鍵暗号方式を用い，適切な場所でのみケーパビリティを復号可能とすることで性質を保証する．提案手法の形式的定義を示し，また，(1)で開発したシステム上に実装した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
高水準言語上でアンビエント計算モデルに基づく分散プログラムを記述するためのフレームワークの土台の構築は順調に完了している．また，そのモデルに忠実に安全な実行を行うためのプログラム実行基盤を実装するための要素技術の開発も順調に進行中である．実装技術の確立は，アンビエント計算モデルにおける実行時の安全性の保証に必要な条件は何かの理解にとって重要であり，これらの成果をもとに，プログラムの「正しい」動作を宣言的に記述し，その記述どおりに安全に実行するための検証機能を備えた実行環境の開発に取り組
むことができると考えている．
|
| 今後の研究の推進方策 |
今後は以下のように研究を進める予定である．
(1) 高水準アンビエント記述（モデル）から上記言語のコードへの変換手法の確立： 汎用言語機能との干渉の解決，モデルに反しない範囲内での生成コードへのユーザによる自由なコード追加，などを考慮しつつ設計を行う.
(2) 高水準アンビエント記述への性質(仕様)の埋込みおよび生成コードへの反映：性質には個々のアンビエントが満たすべき性質を書けるようにする．並行して開発する (3) の検査器は，全てのアンビエントが自分自身の性質を満たすという仮定の下で，システム全体の解析・検証を行う．それぞれのアンビエントが性質を満たすことを各ライブラリでは次のようにして保証する:(Java) 性質に特化した適切なクラスの自動選択（あるいは明示的なクラス指定）(Scheme) 性質をS式中にアノテーションとして埋め込んでおき，ランタイムが性質を満たすかの実行時チェックを行う．
(3) Spinモデル検査器を用いた検証を行うための変換手法の構築：システムが全体として満たすべき性質の解析・検査を網羅的に行うための方法を開発する．階層化されたアンビエント計算のモデルからSpinのフラットなチャネル通信のモデルへの変換は既存研究の改良により行う．再帰オベレータの扱い，アンビエント生成個数の上限，アンビエント間協調動作用通信チャネルの容量など，Spinをターゲットにすることから生じる課題は多く，この開発フェーズだけで良い解決手段が見つからない場合には，必要に応じ高水準記述，ライブラリAPI，性質記述を含めたフレームワーク全体の包括的な再設計も行う．
|
| 次年度の研究費の使用計画 |
平成25年度には，開発者向けAndroid端末を購入し，1年目で完成したJavaおよびSchemeライブラリを用いたプログラムが，資源が乏しくかつ通信制約の厳しいモバイル端末上でも効率良く動作するか実証実験を行う．そのような実機上での実験は実行効率の改善に必要である．さらに，プログラムの解析やモデル検査の評価実験を行うための高性能なPCを1台購入する予定である．
また，最新の研究動向や研究に必要な知識を得るための情報収集や，本研究で得られた研究成果を発表するために，相応の旅費，論文掲載料，図書購入費として使用する予定である．
|
