発展可能ソフトウェアの開発法に関する基礎と支援環境の構築

本研究では,簡単化のため第2階様相述語論理に基づいた発展可能ソフトウェアの新しい要求記述法と,その状態遷移システムによる形式仕様の自動生成に関する基礎理論を発展しつつあり,現在そのための支援システムを開発中である.具体的には,システム要求記述を機能の局所的な性質を記述した理論式として定式化する.また,システム要求の意味は健全でかつ完全な遷移システム(標準モデル)であるという意味論を提案し,その妥当性を理論的かつ実際的側面から議論した.この標準モデルがシステムの形式仕様であり,システム要求の実現である.この意味論は,論理ペトリネットを用いても特性化できることを示した.これは,研究項目(2)と密接に関連する.さらに,複雑な大規模システムの要求記述と仕様化に対処するため,制約によるモジュール化技法,論理ベースの抽象化と階層的詳細化などを研究し,状態爆発と複雑さの問題を部分的に解決した.以上の基礎研究を踏まえ,システム要求記述言語を設計し,システム要求の意味でありかつそれ自身がシステムの形式仕様である「状態遷移システム」を効率よく生成するための理論と実際の導出法を与えた.命題理論に基づいた記述法については既に研究成果を得ていたが,実用性と適用制の範囲を考慮すると,命題論理は余りにも記述能力が低い,しかし,単純に第2階の様相理論に拡張したのでは,計算可能性や高率の点で問題が生じる.そこで,本研究では,一挙に第2階様相述語論理までレベルアップしたことによる問題の他,発展可能なソフトウェアの要求記述,仕様化に柔軟に対処するため,以下の点を考慮した要求記述法並びに記述言語の設計とその意味論に基づいた状態遷移システムベースの形式仕様に変換する手法を与え,ワークステーション上にSICtus Prologを用いて仕様合成システムを開発している.

本研究では,簡単化のため第2階様相述語論理に基づいた発展可能ソフトウェアの新しい要求記述法と,その状態遷移システムによる形式仕様の自動生成に関する基礎理論を発展しつつあり,現在そのための支援システムを開発中である.具体的には,システム要求記述を機能の局所的な性質を記述した理論式として定式化する.また,システム要求の意味は健全でかつ完全な遷移システム(標準モデル)であるという意味論を提案し,その妥当性を理論的かつ実際的側面から議論した.この標準モデルがシステムの形式仕様であり,システム要求の実現である.この意味論は,論理ペトリネットを用いても特性化できることを示した.これは,研究項目(2)と密接に関連する.さらに,複雑な大規模システムの要求記述と仕様化に対処するため,制約によるモジュール化技法,論理ベースの抽象化と階層的詳細化などを研究し,状態爆発と複雑さの問題を部分的に解決した.以上の基礎研究を踏まえ,システム要求記述言語を設計し,システム要求の意味でありかつそれ自身がシステムの形式仕様である「状態遷移システム」を効率よく生成するための理論と実際の導出法を与えた.命題理論に基づいた記述法については既に研究成果を得ていたが,実用性と適用制の範囲を考慮すると,命題論理は余りにも記述能力が低い,しかし,単純に第2階の様相理論に拡張したのでは,計算可能性や高率の点で問題が生じる.そこで,本研究では,一挙に第2階様相述語論理までレベルアップしたことによる問題の他,発展可能なソフトウェアの要求記述,仕様化に柔軟に対処するため,以下の点を考慮した要求記述法並びに記述言語の設計とその意味論に基づいた状態遷移システムベースの形式仕様に変換する手法を与え,ワークステーション上にSICtus Prologを用いて仕様合成システムを開発している.