非形式的仕様記述の効率的形式化に関する研究

点击翻译按钮获取中文摘要

本研究では,システム設計におけるモデル構築の最初に行なわれる,非形式的な問題記述からキーワードを抜き出し,それらの定義を記述する用語辞書,関連の構造化を行なうデータ辞書,関連の修正およびステレオタイプの記述などの静的モデリング,問題記述を確認する検査網羅度表示といった従来の手法では別の枠組で考えられてきた機能を統一した手法を提案した.具体的には、非形式的記述中のマークした用語の品詞,非形式的定義,形式的定義,データ構造を登録し,残りの記述に含まれる同じ用語をマークする.このようなツールをEclipseのプラグインとして,用語およびデータ辞書作成,非形式的な記述の網羅度の確認といった機能をもつツールの機能を実装した.昨年度行なった仕様抽出手段の考案と電動ポットの事例を対象とした実証結果に基づいて,本ツールを利用した仕様の半自動的な形式化について研究した.網羅性の検証においては,簡単な品詞分解による品詞間に共通な語幹の取り出しと意味定義を行なう階層を追加した.実装においては,階層化と他のツールとの連携を重視した.階層化は,将来の複数言語への対応を考慮し,インターフェース部分,自然言語処理,辞書管理等を分離し,また,他のモデリングツールとの一体化を目指して,データの互換性を向上させた.要求獲得から形式的なモデリングへの変換をサポートするツールは少ないことから,年度後半の形式手法に関する国際会議で発表を行なった.組み込みシステムの事例である産業用ロボットの模型を制御するソフトウェアに対して評価を行ない,良好な結果を得た.予定していた旅費は期間の関係により,他の費目に振り替えた.