| 研究課題/領域番号 |
24500032
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
萩原 茂樹 東京工業大学, 情報理工学(系)研究科, 助教 (70334547)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2015-03-31
|
| キーワード | 形式手法 / 組込みシステム仕様 / 修正情報抽出 |
|---|
| 研究概要 |
組み込みシステムの仕様を記述する際、センサー等を通じた環境とのやり取りが複雑であり、一度に誤りなく記述するのは困難であるため、誤りのある仕様から修正に有益な情報を得たい。本研究の目的は、誤りのある仕様から、その原因と箇所を表す情報を計算する方法を形式手法により構成することである。平成24年度においては、原因を表す情報を計算する方法の研究を行った。
まず、準備済みの誤り原因情報抽出手法がどの規模の組み込みシステム仕様に適用可能かを特定した。具体的には、時間論理に基づいたオブジェクト指向オープンシステム仕様記述言語Tで、現実規模のエレベータシステム仕様を記述した。そして、我々が既に構成しプロトタイプを実装した、強充足可能性に基づいた情報抽出手法を、その仕様に適用した。計算コストの膨大さ故、現実規模の仕様からは抽出困難であると予想されたが、その結果、2階用エレベータの仕様の規模までは、誤り情報抽出が可能であることがわかった。
次に、無限長語オートマトンの縮約技術の適用による、抽出手法の効率化に取り組んだ。計算コストが高いのは、無限長語オートマトンの補オートマトンを計算する過程であり、入力となる無限長語オートマトンを小さな形にすることが重要である。我々は、意味を変えずに無限長語オートマトンを小さくする二つの技術を研究した。具体的には、オートマトンの遷移関係に二分決定グラフを用いて、演算速度の高速化及び使用メモリを効率化し、さらに、等価な状態を一つの状態としてまとめる工夫と、不必要な状態を作成しない工夫をそれぞれ研究した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
平成24年度の研究目標は、(1)準備済みの誤り原因情報抽出手法がどの程度の規模の仕様に対応できるかを特定することと、(2)現実規模の仕様に対応できるようにするために、最も重要な技術である無限語長オートマトンの縮約技術の開発であった。これに対して、研究実績の概要で述べたように、(1)と(2)のそれぞれにおいて、一定の成果が出たため、「概ね順調に進展している」と判断した。
|
| 今後の研究の推進方策 |
平成25年度については、誤りのある組込みシステム仕様からの誤り原因情報抽出手法の構成において、抽出情報の単純化による抽出手法の効率化に取り組む。現実規模の仕様を適用可能で、かつ、得られる環境制約が修正に有益であるためには、どのような単純化が必要かを考察する。次に、抽出手続きの正当性の証明を行う。ここで、証明する正当性とは、手続きの停止性、得られる制約の健全性(手続きが抽出した制約は正しい環境制約であるという性質)、得られる制約の最弱性(手続きが抽出した制約は、想定している式のクラスで最弱であるという性質)の3つである。これにより、構成する手続きに、理論的な裏付けを与える。
平成26年度については、24年度、25年度の成果をソフトウェアとして設計・実装する。また、誤り箇所の情報抽出手法の研究を行う。具体的には、第一に、誤り箇所の情報抽出手法の構成に取り組む。仕様に誤りがある場合、つまり仕様が強充足不能である場合、その仕様の振る舞いを表す無限長語オートマトンには、仕様が強充足不能である証拠となる、環境振る舞いを表すオートマトンの部分グラフが得られる。その部分グラフの存在を導いた仕様の部分を特定する方法を考案する。さらに、仕様のその部分が極小になるように、特定する方法を精錬する。第二に、現実規模の仕様を適用可能にするための手続き効率化に取り組む。無限長語オートマトンのサイズを小さくする手法を適用し、この手法が現実規模の仕様に適用可能となるように手続きを効率化する。第三に、抽出手続きの正当性の証明に取り組む。これまでに得られた手続きの正当性を証明する。ここで、証明する正当性は、(a)特定された仕様の範囲は強充足不能であることと、(b)その範囲が極小であることである。極小範囲を特定する方法が得られなかった場合は、(b)の代わりに、(b')その範囲の特定が工学上有意であることを示す。
|
| 次年度の研究費の使用計画 |
平成25年度は計算サーバを購入し、これまでの成果を計算機上に実装し、ソフトウェアとして構成する。さらに、この成果を研究会や国際会議で発表する際、ノートPCが必要となるため、これを購入する。
また、研究の基礎となる理論や、最新の研究動向を把握するため、書籍を購入する。消耗品であるプリンタトナーやドラム、そしてハードディスクは、プリンタ、サーバやPCを運用するために必要なため、購入する。
本研究の成果を発表するため、さらに、最新の研究動向を把握するため、国内研究会を年2-3回、国際会議を年2回出席し調査・発表する。このために旅費を用いる。研究会など大学外でも研究作業を行うために、ワイヤレスWAN接続が必要である。このため、モバイル通信機器と通信費を計上する。
また、平成24年度の未使用額は上記の予算に組み込む。
|
