2014 Fiscal Year Annual Research Report
自己反映的ソフトウェアのための実行時検証とそのための仕様記述方式
| Project/Area Number |
24500033
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
渡部 卓雄 東京工業大学, 情報理工学(系)研究科, 准教授 (20222408)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | 自己反映計算 / 広域自己反映計算 / アクターモデル / 文脈指向プログラミング / 並行文脈指向プログラミング / 実行時検証 |
|---|
| Outline of Annual Research Achievements |
最終年度は，前年度に引き続き実行時検証に適したメタレベル計算の表現方法を含む自己反映的プログラムの構成方式の研究を行った．具体的には研究実施計画を踏まえ以下のようなタスクを実施した．
(1) 広域自己反映計算の形式化とその検証方式：アクターモデルを基盤とした広域自己反映計算モデルの形式化方式およびその検証手法の提案を行った．広域自己反映計算とは，複数の計算主体（ここではアクター）からなる系の総体的な振る舞いに対するメタレベルを介した自己反映計算方式である．この手法は研究代表者が1991年に提案していたものであるが，メタレベルの構成が実装方式に依存したアドホックなものであった．前年度に，個々のアクターのメタレベルを並列合成することによりアクターのグループのメタレベルを構成する手法を提案したが，本年度はその詳細な定式化とその検証方式を提案した．
(2) 上記(1)において得られた知見を元に，並行計算系における文脈指向プログラミング(COP)の一方式である並行文脈指向プログラミング(CCOP)を提案し，その実現方式の提案と評価を行った．具体的には実行時文脈の変化をアクターからなるグループ内において非同期的に伝搬する手法を広域自己反映計算手法を用いて実現している．加えてプログラミング言語Erlangによるプロトタイプを元に提案手法の評価を行い，その有効性を確認した．
(3) 上記(1)の成果を動的な実行時検証に応用して一定の成果を得た．具体的には，故障動作を伴う並行システムの仕様記述のモジュール化とモデル検査系の提案と実装，および人為的な誤りを含む手続きの形式化と検証方式の提案である．両者共に，自己反映計算の考え方によって故障動作（および人為的誤り）記述の適切なモジュール化が可能になることを示すことができた．
|
Research Products
(10 results)
