| 研究概要 |
(1) 発展可能ソフトウエアの要求記述法と形式仕様の自動生成法に関する継続研究
平成9年度では,命題論理に基づいた新しい要求記述法と,その状態遷移システムによる形式仕様の自動生成に関する基礎理論を展開し,その処理系を開発した.しかし,実用性や適用範囲の広さを考慮すると,命題論理では余りにも記述能力が低い.しかしながら,単純に第一階述語論理や高階(様相)論理に拡張したのでは,計算可能性や効率の点で問題が生じる.そこで,本年度は,平成9年度の研究成果である要求記述法や処理系を拡張し,制限された第二階様相論理に基づいた要求記述法と記述言語の設計ならびにその処理系をjavaを用いて分散環境上に実現した.研究開発に当たり考慮した点は以下の通りである.
(a) 機能の記述は述語論理の範囲で行なった,制約の記述を第二階様相論理で行なった.ただし,命題論理の場合と同じような意味論が第二階様相述語論理に拡張しても展開でき,要求記述のモデルである形式仕様への変換が効率的に行なえること.その際問題になる効率や状態の爆発を,述語によるラベル機能を用いて克服した.
(b) 大域的制約,局所的制約を用いたモジュール化技法.抽象化と階層的詳細化の導入.
(c) 要求の変化に柔軟に対処可能なやわらかい要求記述法と仕様化技術の達成.
(d) 状態遷移と状態の機能に対する外延的性質による新しい等価性の理論の確立.
(2) 発展可能ソフトウェアシステム要求診断・検証システムの基本設計
曖昧で不完全な要求記述を対象とし,その意味である状態遷移システムのユーザの解釈に基づき,正しくない状態遷移,抜けている状態遷移,矛盾した意味を持つ状態などの診断項目により,要求記述を診断するシステムの基本設計を行なった.また,要求記述の時間に関する動的かつ大域的な性質を検証するための時制論理による検証システムの基本設計を行なった.両システムの実装は,平成11年度に行なう.
|
