2012 Fiscal Year Research-status Report
自己反映的ソフトウェアのための実行時検証とそのための仕様記述方式
| Project/Area Number |
24500033
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
渡部 卓雄 東京工業大学, 情報理工学(系)研究科, 准教授 (20222408)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | 自己反映計算 / 文脈指向プログラミング / 実行時検証 / アクターモデル / 実時間システム / 形式手法 / 形式仕様 / 時相論理 |
|---|
| Research Abstract |
平成24年度は，主に基盤となる技術である実行時検証に適したメタレベル計算の表現手法を含む自己反映的プログラムの構成方式の研究を行った．具体的には研究実施計画にある通り以下のようなタスク(A1)～(A3)を実施した．
(A1) 基本的な自己反映計算の枠組みとその検証方式：当初の予定通り，アクターモデルを基盤とした自己反映計算モデルとそのための実行時検証方式の枠組みを定式化し，その性質を調査した．特に自己反映計算の重要な応用である実行環境への適応については，近年注目されている文脈指向の考え方にもとづいた定式化を行っている．特に本研究では，時間（時区間）を文脈と捉えることで適応的な実時間システムへの応用を可能にしてる．これは特に実時間組み込みシステムへの応用が効果的であることが明らかになりつつある．さらに，本研究における自己反映計算機構の実現には，言語の意味記述とその拡張方式の定式化が重要である．これに関して，定理証明支援系Coqで記述された検証済みの言語定義を，その証明を再利用しつつ拡張する方式を提案している．
(A2)メタレベル計算動作の抽象化記述方式：タスク(A1)で述べた自己反映計算モデルの動作を，時間を考慮した状態遷移系として定式化した．
それにもとづく言語機構を文脈指向プログラミングの考え方にもとづいて実現し，JavaおよびScala上で実装した．
(A3)プロトタイプの評価：以上(A1)(A2)で実現した自己反映計算のフレームワークを用いて，適応的なWebアプ リケーション，実時間組み込みシステム等の例題の記述と計算機実験を行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
現在までの成果は，研究実績の概要にあるようにほぼ研究実施計画に沿っている．時間をプログラムの実行時文脈と捉えることで，（自己反映計算のひとつの応用である）文脈指向プログラミングの考え方を実時間システムに適用するというアイデアは研究計画時点ではなかったものであるが，本研究の適用範囲を拡大する上で重要である．また，検証済みの言語定義に関する証明の再利用方式を確立したことも特筆すべきである．以上より，現在までの達成度はおおむね順調であると判断できる．
|
| Strategy for Future Research Activity |
当初の予定通り，もう一つの基盤技術である安全性に関する性質の記述形式およびその実行時検証手法についての研究(以下のタスクB1~B3)を行う．
(B1)ベースレベルにおける性質記述：ベースレベル(アプリケーション本来の動作レベル)の性質は，プログラムコード中の表明として記述する．一般にこの手法ではプログラムコード量が増大するにつれて表明の記述量が増大するという欠点がある．これに対しては，本年度に確立した証明の再利用方式を適用することで，この問題に対処する．
(B2)メタレベルにおける性質記述：タスク(A2)で述べたように，メタオブジェクトの記述は状態遷移系として抽象化されている．よって，その上の諸性質は時相論理式などで自然に与えることがでいるが，これと(B1)の表明による性質記述との整合性をとる必要がある．我々は仕様記述言語Moxaにおいてオブジェクトの動作仕様に関するアスペクトとして状態遷移系を導入する手法を確立している．ここでその手法をメタオブジェクト仕様に適用し，ベースレベルの表明による仕様記述と共存させる技術を確立する．
(B3)実行時検証機構のプロトタイプ実装：上で述べたように，メタオブジェクトは状態遷移系として表現され，その性質は時相論理式によって記述される．正確には，ここで用いるのは過去時相論理(Past-Time Temporal Lo gic)と呼ばれるもので，現時点から過去にさかのぼった振る舞いについての性質を記述する．これは実行時検証に有効であり，我々の以前の研究においてもこの論理をベースとした記述を採用している．本研究でも過去時相論理の一種であるPT-LTLあるいはPT-DTLを用いる．
|
| Expenditure Plans for the Next FY Research Funding |
H24年度については，研究計画の軽微な改善によって効率的な予算執行が可能となり，結果として未使用額が発生した．具体的には，研究代表者自身が実験用プログラムを作成する時間がとれたことにより，プログラム作成補助のための謝金が不要となったこと，および消耗品として購入を予定していた開発用ソフトウェアをより効果的な代替品に置き換えることができたことによる．
H25年度以降は，今後の研究の推進方策で述べたように実行時検証機構のプロトタイプの実装および評価を行う．特に研究実績の概要で述べたように実時間組み込みシステム等を応用対象として評価を行うことが効果的であることが明らかになってきたため，開発・実験用のパーソナルコンピュータに加え，実時間組み込みシステムのプロトタイプとなる，センサーや小規模ネットワークを備えたマイクロコンピュータボードが複数台必要となる．H24年度の未使用額については主としてこれらに充てる予定である．
|
Research Products
(12 results)
