| 研究概要 |
将来のソフトウェア産業の基盤技術として必要不可欠である,コンポネントが必要とされている仕様を満たしていることを厳密に検査する基礎技術およびツールの開発を行った.本研究では,仕様のコンポーネント化を支援するための諸機能を有する仕様記述言語CafeOBJを基盤ツールとして用いた.CafeOBJは,研究代表者を中心に開発を続けている代数仕様記述言語で,抽象データ型のみならず抽象機械の記述にも適しており,仕様のコンポネント化を支援する強力なモージュルシステムを有するのも特徴の一つである.具体的な研究成果は以下のとおりである.(1)定理証明器の設計・開発:CafeOBJの項で表現された一階述語論理式に対し導出を行う機能(PigNose)をCafeOBJシステムに組込み,いくつかの例題に適用し有効性を確認した.(2)コンポネントに基づくシステム開発法:コンポネントを組み上げて高品位のソフトウェアを作成するための基礎理論を作り,その理論に基づいてソフトウェアを作成するツールの設計および作成を行った.(3)検証実験:CafeOBJ支援のもとで検証する方法を整理・提案し,鉄道信号システムやセキュリティシステム等に適用することで有効性を確認した.
|
