| 研究課題/領域番号 |
11694173
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 法政大学 (2000-2001)
広島市立大学 (1999) |
|---|
研究代表者 |
劉 少英 法政大学, 情報科学部, 教授 (90264960)
|
|---|
| 研究分担者 |
大場 充 広島市立大学, 情報科学部, 教授 (50264966)
荒木 啓二郎 九州大学, 大学院・システム情報科学研究院, 教授 (40117057)
玉井 哲雄 東京大学, 教養学部, 教授 (60217172)
新井 紀子 国立情報学研究所, 情報学基礎研究系・情報数理研究部門, 助教授 (40264931)
|
|---|
| 研究期間 (年度) |
1999 – 2001
|
| 研究課題ステータス |
完了 (2001年度)
|
| 配分額 *注記 |
8,900千円 (直接経費: 8,900千円)
2001年度: 2,300千円 (直接経費: 2,300千円)
2000年度: 3,100千円 (直接経費: 3,100千円)
1999年度: 3,500千円 (直接経費: 3,500千円)
|
|---|
| キーワード | SOFL / Formal Engineering Methods / Workflow / Formal Specification / To-down design / Object-oriented Design / Specification Transformation / Software tool / Object-Oriented Design / 形式工学手法 / ソフトウェア検証 / 厳密なレビュー / 仕様テスト / 仕様分析 / 形式的仕様 / システム開発 / ソフトウェア進化 / 形式的工学手法 / ソフトウェアテスト / 形式的検証 / ソフトウェア開発環境 / ソフトウェア分析 |
|---|
| 研究概要 |
このプロジェクトの研究によりいくつかの成果を獲得した。第一、実用的な形式的仕様記述言語と手法SOFL(Structured Object-oriented Formal Language)の文型、意味、及び方法論を実際のソフトウェアシステムの開発に応用できるレベルまで発展した。文型はBMFで定義し、意味は、ZとObject-Zで形式的に定義した。方法論に関しては、形式的仕様を構築するの非形式、半形式、及び形式の「三段階(three-steps)」方法を確立し、SOFLを用いてソフトウェア開発の有効なプロセスも提案した。第二、形式的証明と安全性を分析するために使われるfault tree技術を基に形式的仕様を検証する新しい厳密的なレビュー技術を開発した。この技術では、SOFLの仕様だけではなく、他の形式的仕様も厳密的に検証することができる(例えば、VDM, Z、B)。第三、形式的証明を伝統的なプログラムテストの原理と統合して、実行可能と実行不可能の二種類の形式的仕様をテストすることができる。従って、ソフトウェア開発の要求仕様や設計などの上流文章のテストを行うことができる。これらのレビューとテスト技術でソフトウェア開発の費用を大幅に減少することができる。第四、SOFLは、ソフトウェア開発のプロセスの定義、予想、及び制御にどのように応用できるということを研究し、この分野にもっと発展する潜在力を発見した。第五、SOFLの実用性を確認するために、SOFLを用いて、「大学情報管理システム」や「インタネット銀行システム」や「財務管理システム」などの要求仕様と設計を作成し、ある部分をC++又はJavaで実装した。これらの応用事例によって、SOFLの弱点を改善することができた。最後は、SOFLの仕様を構築することやテストなどを支援するツールの原型を開発し、これらのツールでいくつかの事例システムを構築して、テストした。これらの応用により、ツールの改善または発展すべき点を明らかにした。現在これらのツールは、まだ原型だが、より上質及び豊富的な機能を持つSOFLの支援環境の開発の堅実的な基礎になった。
|
