2006 Fiscal Year Annual Research Report
| Project/Area Number |
17700028
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
清野 貴博 独立行政法人産業技術総合研究所, システム検証研究センター, 契約職員 (10397226)
|
|---|
| Keywords | ソフトウェア開発効率化・安 / ユーザインターフェイス / 形式手法 |
|---|
| Research Abstract |
本年度は、これまでに提案した検証支援ツールがEclipseから呼び出せるようにプラグインを実装した。プラグインは、研究代表者のウェブサイトにおいて、引き続き無償配布を行っている※。OTS/CafeOBJ法は代数仕様言語CafeOBJの処理系を用いるため、開発したツールはCafeOBJの処理系を利用するために基本的な機能を提供するツール群と、OTS/CafeOBJ法に特化した支援機能を提供するツール群の2つから構成することとした。これらのツールでは前述の目的を達成するため、Eclipseの標準的なマナーに沿ったGUIを採用した。
産総研の事務システムを対象とする事例研究では、要件定義において用いられる図表に形式手法の考え方を導入した。現場の抵抗が激しく予想外の困難を強いられたが、形式仕様に変換可能な記述がされた、実際のシステムの要件定義書を手に入れた。来年度は、これらを元にして、形式仕様への変換および検証を、また可能であるならばテストケースの生成までを行う予定である。
検証支援ツールの発展として、より強固な論理的背景を持たせるために、Martin-Lof型理論に基づく証明支援系AgdaからCafeOBJを呼び出すためのAgdaプラグインを試作した。これにより、CafeOBJだけでは不可能であった、個々の証明譜記述および証明の正しさや、個々の証明間の関係を数学的基盤の上で厳密に取り扱うことが可能であることを確認できた。しかし、Agdaのプラグイン機構が未成熟であるため、現時点においては実用に足る機能を提供するには至っていない。
※http://www.jaist.ac.jp/~t-Seino/research/cafeobj/
|
