2013 Fiscal Year Research-status Report
形式手法による欠陥のある現実規模の組み込みシステム仕様からの修正情報抽出
| Project/Area Number |
24500032
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
萩原 茂樹 東京工業大学, 情報理工学(系)研究科, 助教 (70334547)
|
|---|
| Keywords | 形式手法 / 組み込みシステム仕様 / 修正情報抽出 |
|---|
| Research Abstract |
組み込みシステムの仕様を記述する際、センサー等を通じた環境とのやり取りが複雑であり、一度に誤りなく記述するのは困難であるため、誤りのある仕様から修正に有益な情報を得たい。本研究の目的は、誤りのある仕様から、その原因と箇所を表す情報を計算する方法を形式手法により構成することである。平成25年度においても前年度と同様、誤り原因の箇所を表す情報を抽出する手法の効率化を行った。計算コストが高いのは、無限長語オートマトンの補オートマトンを計算する過程であり、入力となる無限長語オートマトンを小さな形にすることが重要である。平成25年度においても、時間論理式から無限長語オートマトンへの変換の効率化を行った。同一視できる状態をひとつに行なうことによって、オートマトンを簡約するが、同一視できるかを、オートマトンを作成している途中の情報のみで判断可能で、縮退効果がある技術を構成した。また、この技術を基礎とした誤りのある仕様から、その原因を表す情報を計算する手法の正当性を示した。示した正当性は、手続きの停止性、得られる制約の健全性(手続きが抽出した制約は正しい環境制約であるという性質)、得られる制約の最弱性(手続きが抽出した制約は、想定している式のクラスで最弱であるという性質)の3つである。これにより、構成する手続きに、理論的な裏付けを与えた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成25年度の研究目標は、(1)誤り原因情報抽出手法の効率化及び、(2)その正当性の証明であった。(1)(2)それぞれにおいて、一定の成果が出た。よって、おおむね順調に進展していると判断した。
|
| Strategy for Future Research Activity |
平成26年度については、24年度、25年度の成果をソフトウェアとして設計・実装する。また、誤り箇所の情報抽出手法の研究を行う。具体的には、第一に、誤り箇所の情報抽出手法の構成に取り組む。仕様に誤りがある場合、つまり仕様が強充足不能である場合、その仕様の振る舞いを表す無限長語オートマトンには、仕様が強充足不能である証拠となる、環境振る舞いを表すオートマトンの部分グラフが得られる。その部分グラフの存在を導いた仕様の部分を特定する方法を考案する。さらに、仕様のその部分が極小になるように、特定する方法を精錬する。極小範囲を特定する方法が得られなかった場合は、修正に有意義な、自明ではない範囲が得られるように注意しながら、特定手法を構成する。第二に、現実規模の仕様を適用可能にするための手続き効率化に取り組む。平成24,25年度に構成した無限長語オートマトンのサイズを小さくする手法を適用し、この手法が現実規模の仕様に適用可能となるように手続きを効率化する。第三に、抽出手続きの正当性の証明に取り組む。これまでに得られた手続きの正当性を証明する。ここで、証明する正当性は、(a)特定された仕様の範囲は強充足不能であることと、(b)その範囲が極小であることである。極小範囲を特定する方法が得られなかった場合は、(b)の代わりに、(b')その範囲の特定が工学上有意であることを示す。
|
| Expenditure Plans for the Next FY Research Funding |
平成25年度に行うと想定していた学会発表が、平成25年度にできなかったため、次年度使用額が生じた。
平成26年度は計算サーバを購入し、これまでの成果を計算機上に実装し、ソフトウェアとして構成する。さらに、この成果を研究会や国際会議で発表する際、ノートPCが必要となるため、これを購入する。また、研究の基礎となる理論や、最新の研究動向を把握するため、書籍を購入する。消耗品であるプリンタトナーやドラム、そしてハードディスクは、プリンタ、サーバやPCを運用するために必要なため、購入する。本研究の成果を発表するため、さらに、最新の研究動向を把握するため、国内研究会を年2-3回、国際会議を年2回出席し調査・発表する。このために旅費を用いる。研究会など大学外でも研究作業を行うために、ワイヤレスWAN接続が必要である。このため、モバイル通信機器と通信費を計上する。また、平成25年度の未使用額は上記の予算に組み込む。
|
