1997 Fiscal Year Annual Research Report
FM-ISEE:形式的手法と知的ソフトウェア工学環境
| Project/Area Number |
08044167
|
|---|
| Research Institution | Hiroshima City University |
|---|
Principal Investigator |
劉 少英 広島市立大学, 情報科学部, 助教授 (90264960)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
MICHAEL Hinc New Jersey Institute of Technology, 情報科学部, 教授
CHRIS HoーStu Queensland University of Technology, 情報科学, 講師
YONG Sun The Queen's University of Belfast, 情報科学部, 講師
A Jeff Offut George Mason University, 情報科学部, 助教授
荒木 啓二郎 九州大学, 大学院・システム情報科学研究科, 教授 (40117057)
|
|---|
| Keywords | 形式的手法 / 形式的仕様 / ソフトウェア支援環境 / ソフトウェア検証 / ソフトウェアテスト / 厳密なレビュー / 形式的意味 / SOFL |
|---|
| Research Abstract |
本プロジェクトは,信頼性の高いソフトウェアシステムを開発するための形式的手法で、既存のものより強力でユーザ親和性の高い実用的なものを開発し、さらに形式的手法を支援するための知的ソフトウェア工学環境の構築に関する研究を平成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国際会議等様々のジャナルと国際会議で篇論文を発表した。
|
-
[Publications] Saoying Liu et al: "SOFL:A Formal Engineering Methodology for Industrial Applications" IEEE Transactions on Software Engineering. 24・No.1. (1998)
-
[Publications] Saoying Liu: "Evolution:A More Practical Approach than Refinement for Software Development" Proceedings of Third IEEE International Conference on Engineering of Complex Computer Systems. Sept.142-151 (1997)
-
[Publications] Saoying Liu: "A Formal Definition of FRSM and Applicatios" International Journal of Software Engineering and Knowledge Engineering. 8・3. (1998)
-
[Publications] Saoying Liu and John A.McDermid: "A Formal Specification of Fault Trees for SAM" Transactions of Information Processing Society of Japan. 38・10. 2014-2030 (1997)
-
[Publications] Chris Ho-Stuart Shaoying Liu: "A Formal Operational Semantics for SOFL" Proceedigs of 1997 Asia-Pacific Software Engineering Conference. 12月. 52-61 (1997)
-
[Publications] Saoying Liu: "Formal Methods and Intelligent Software Engineering Environments" Information-An International Journal. 1・1(予定). (1998)
-
[Publications] Yong Sun, Shaoying Liu: "Self-independent Petri Nets for Distributed Systems" Proceedings of FORTE/RSTV'97. 487-502 (1997)
-
[Publications] Jeff A.Offutt Shaoying Liu: "Generating Test Data from SOFL Specifications(予定)" The Journal of Systems and Software,Elsevier Science Inc.
