| 研究分担者 |
HINCHEY Mich New Jersey Institute of Technology, 情報科学部, 教授
HOーSTUART Ch Queensland University of Technology, 情報科学, 講師
SUN Yong The Queen's University of Belfast, 情報科学部,, 講師
OFFUTT A Jef George Mason University, 情報科学部,USA, 助教授
荒木 啓二郎 九州大学, 大学院・システム情報科学研究科, 教授 (40117057)
|
|---|
| 研究概要 |
本プロジェクトは,信頼性の高いソフトウェアシステムを開発するための形式手法で、既存のものより強力でユーザ親和性の高い実用的なものを開発し、さらに形式的手法を支援するための知的ソフトウェア工学環境の構築に関する研究を平成9年度にも著しく進展して、素晴らしい成果を獲得したと思います。具体的に重要な結果は以下のものである。
1.階層的なデータフロー図を基にした構造化方法論とオブジェクト指向方法論、モデル指向形式言語VDL-SLとの適切な統合を研究しており、ユーザ親和性の高い実用的な形式的手法SOFL(Structured-Object-based-formal Language)を設計と改良した。
2.既存の形式的手法Zと提案したSOFLを複雑な情報シスタムの開発に応用して、その結果を評価した。
3.形式的手法よりも実用的な「形式的工学手法」を初めて提案した。形式的手法を比べて、以下の三つの発展がある。(1)数学のみを用いた安全な要求仕様を記述ではなく、図や自然言語や数学を統合させた言語を用いて主要な要求仕様を記述している。(2)形式的詳細化(Refinement)ではなく、進化させて行く方法(Evolution)で開発して行くという点である。(3)形式的証明(Formal Proofs)ではなく、厳密なレビューを行なうと言うことになる。
4.構造化形式的手法SOFLを基にしたソフトウェアテスト技法に関する研究を通して,形式的仕様のテスト及び形式的仕様を基に開発されたソフトウェアのテストの両者を行うための、具体的なテスト生成のルールを作成した。この二つは,密接に関係しているが,従来のテスト生成の技法とは目的が異なる。前者は仕様の整合性を検証するため,形式的仕様を実行せずに,仕様テストする手法である。後者は,形式的仕様を基に作成されたソフトウェアの正しさを保証するテスト手法である。
5.SOFLの支援環境を構築するため,SOFLの形式的意味を研究し,公理的意味と操作的意味モデルを確立した。
6.SOFLの支援環境を構築するための技術を研究し,SOFLのグラフィカル・ユーザインタフェイスとテストシスタムのプロトタイプを構築した。
以上の研究に基づいてIEEE Transactions on Software EngineeringやIEEE国際会議等様々のジャナルと国際会議で8篇論文を発表した。
|
