2005 Fiscal Year Annual Research Report
| Project/Area Number |
17700028
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
清野 貴博 独立行政法人産業技術総合研究所, システム検証研究センター, 産総研特別研究員 (10397226)
|
|---|
| Keywords | 形式手法 / 代数仕様 / 項書換え / CafeOBJ / 観測遷移機械 |
|---|
| Research Abstract |
今日、ソフトウェアの信頼性確保は急務であり、形式手法を用いた検証法がさかんに研究されている。それらのうち、項書換え系を用いた検証手法は、習得しやすく、かつ見通しのよい検証が可能である。研究代表者は、その中で分散システムに関する仕様記述・検証手法であるOTS/CafeOBJ法に着目し、いくつかの計算機を用いた検証支援ツールを提案してきた。本研究は、それらの検証支援ツールを、形式手法が専門でないソフトウェア技術者にも馴染みやすくするため、実務者の間で定評のある統合開発環境Eclipse上に実装し、実用規模の仕様記述に耐えうるツールであることを確かめることを目的としている。
本年度は、Eclipseのプラグインの実装法を習得し、これまで提案した検証支援ツールの一部を実装した。これらのツールは、研究代表者のウェブサイトにおいて、無償配布を開始した※。OTS/CafeOBJ法は代数仕様言語CafeOBJの処理系を用いるため、開発したツールはCafeOBJの処理系を利用するために基本的な機能を提供するツール群と、OTS/CafeOBJ法に特化した支援機能を提供するツール群の2つから構成することとした。これらのツールでは前述の目的を達成するため、Eclipseの標準的なマナーに沿ったGUIを採用した。
研究代表者は、北陸先端科学技術大学院大学 情報科学研究科 二木研究室において本ツールのデモを行った。
※http://www.jaist.ac.jp/~t-seino/research/cafeobj/
|
