2000 Fiscal Year Annual Research Report
| Project/Area Number |
11694173
|
|---|
| Research Institution | Hosei University |
|---|
Principal Investigator |
劉 少英 法政大学, 情報科学部, 助教授 (90264960)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
大場 充 広島市立大学, 情報科学部, 教授 (50264966)
荒木 啓二郎 九州大学, 大学院・システム情報科学研究院, 教授 (40117057)
玉井 哲雄 東京大学, 教養学部, 教授 (60217172)
新井 紀子 国立情報学研究所, 情報学基礎研究系情報数理研究部門, 助教授 (40264931)
|
|---|
| Keywords | 形式工学手法 / ソフトウェア検証 / 厳密なレビュー / 仕様テスト / 仕様分析 / 形式的仕様 / システム開発 / ソフトウェア進化 |
|---|
| Research Abstract |
平成12年度は、伝統的な形式的手法よりも高い実用性を持つ形式工学手法SOFLを支援するために、仕様品質の保証、仕様の性質の検証、ソフトウェアコンポーネントによってシステムの開発手法、及びSOFLの支援ツール等様々な課題に関する研究を行った。仕様品質を評価及び改善するために、SOFLを用いて「財務分析システムの仕様」を記述、「ソフトウェア開発プロセス」を定義、及び「ネットワークプロトコル仕様」を記述することを行った。それらの結果によって、優れた保守性と変換容易性を持つSOFL仕様の優良的な構造を発見及び定義した。さらに、形式的証明とシステムの安全性を分析する技術を統合し、証明よりも高い実用性を持つ厳密なレビュー手法を提案した。この技術では、形式的仕様の有効性と一致性及び予想されるシステムの安全性を分析するのに必要なタスクを木構造で表示、分析するプロセスを管理、そして分析によって発見された問題を報告することができる。ソフトウェアコンポーネントによってシステム開発する方法論については、コンポーネントの定義、仕様記述、及びコンポーネントの組合等問題点を検討した。そして、同類システム(Families of Systems)を開発するため、読みやすい図の言語UMLとSOFLを統合して、オブジェクト指向方法論を支援するのに必要なSOFL言語構造を発展した。SOFL仕様を正確に記述することを支援するために、SOFLのGUIやテストツールの原型(prototype)等を構築した。このツールでは簡単なSOFL仕様を作成、仕様の有効性をテストすることによって、ツールの評価も行った。
|
Research Products
(3 results)
-
[Publications] Shaoying Liu,Jim Woodcock: "Supporting Rigorous Reviews of Formal Specifications using Fault Trees"Proceedings of Conference on Software Theory and Practice, IFIP 16^<th> World Computer Congress. August. 459-470 (2000)
-
[Publications] Shaoying Liu,Tetsuo Fukuzaki,Toji Miyamoto: "A GUI and Testing Tool for SOFL"Proceedings of Asia-Pacific Software Engineering Conference, IEEE Press. December. 421-425 (2000)
-
[Publications] Hassan Gomaa,Shaoying Liu,Michael Shin: "Integration of Domain Modeling Method for Families of Systems with the SOFL Formal specification Language"Proceedings of 6^<th> IEEE International Conference on Engineering of Complex Computer Systems IEEE. Sept.. 61-71 (2000)
