2014 Fiscal Year Research-status Report
時間論理によるリアクティブシステム仕様のプログラム化可能性の判定とプログラム合成
| Project/Area Number |
25330008
|
|---|
| Research Institution | Saitama University |
|---|
Principal Investigator |
吉浦 紀晃 埼玉大学, 理工学研究科, 准教授 (00302969)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | 仕様記述 / 仕様検証 / 時間論理 / リアクティブシステム / プログラム化可能性 |
|---|
| Outline of Annual Research Achievements |
本年度は、時間論理で記述されたリアクティブシステムプログラム仕様から、その仕様に含まれる仕様の情報を効率的に導出するための証明システムの実装した。この証明システムはrelevant logicをベースとしている。仕様がプログラム化不能である場合、仕様記述者が仕様を修正する必要があるが、仕様に含まれる誤りの発見を支援することが可能である。この成果は国際会議での発表が採択されている。
次に、リアクティブシステム仕様がプログラム化可能であることの必要条件として段階的充足可能性がある。この性質の判定方法の実装は既に研究代表者により行われていたが、実装上の工夫や判定方法の改良を行うことで高速化を行った。この成果は国際会議での発表が採択されている。
次に、リアクティブシステム仕様がプログラム化可能であることの必要条件として強充足可能性があり、強充足不能な仕様を仕様を強充足可能に修正することは重要である。本研究では、その修正する方法を提案した。具体的には、リアクティブシステム利用者の動作に対する制限を仕様に加えることより仕様を修正する。この制限は仕様から自動的に導出される。この成果は、国内の研究会で発表済みであり、国際会議での発表が採択されている。
また、仕様の強充足可能性の判定の高速化を行った。従来、この判定には仕様から状態遷移図を構成する必要があるが、本研究では仕様が強充足不能である場合には、高速で判定可能な手続きを提案した。この手続きは様相論理の分解証明法に基づく。この成果は、国内の研究会に発表済みである。
また、本研究での成果を利用して、Javaプログラムのデータの競合の検出方法を構築した。これは、従来提案されている検出方法よりもより多くのデータの競合を検出可能であり、この方法を実装するとともに実験によりその有効性を示した。この成果は、国際会議において発表済みである。
|
| 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 |
これまでに提案した強充足充足可能性の高速な判定手続きを実装、段階的充足可能性の判定手続きの実装のさらなる高速化、そして、リアクティブシステム仕様がプログラム化可能でない場合の修正方法の実装など、これまでの研究期間に提案してきた理論的な方法を実装し、これらを融合することで、リアクティブシステム仕様のプログラム化可能性の高速判定器の構築を行う。
|
| Causes of Carryover |
本研究ではリアクティブシステムプログラム仕様の性質の判定システムの実装を行うが、その実装用の計算機を平成２６年度に購入予定であった。しかし、判定システムのアルゴリズムの改善に重点を置き研究を行い、実装をその後に行うことになった。このため、実装の進捗状況に合わせて計算機の購入を行うこととした。よって、実装を本格的に行う平成２７年度に計算機を購入することとした。ゆえに、平成２６年度に支出予定であった計算機の購入費が次年度使用額として生じた。
|
| Expenditure Plan for Carryover Budget |
本年度に、平成２６年度に購入予定であった計算機を購入する予定であり、次年度使用額はこの購入に充てる。それ以外の予算については当初の計画通りに支出予定である。
|
