| Co-Investigator(Kenkyū-buntansha) |
GLENN Evans The Queen's University of Belfast, 情報科学部, 助手
JIAN Chen Monash University, 情報科学部, 講師
新井 紀子 広島市立大学, 情報科学部, 助手 (40264931)
CHRIS HoーStu Queensland University of Technology, 情報科学, 講師
YONG Sun The Queen's University of Belfast, 情報科学部, 講師
OFFUTT A Jef George Mason University, 情報科学部, 助教授
荒木 啓二郎 九州大学, 大学院・システム情報科学研究科, 教授 (40117057)
大場 充 広島市立大学, 情報科学部, 教授 (50264966)
|
|---|
| Research Abstract |
本プロジェクトは,新しい形式的使用記述言語SOFL (Structured-Object-Oriented Language)を用いた形式手法に基づき,大規模かつ複雑なソフトウェアシステムを開発するための実用的技術と方法論の構築を目指す.当初の研究計画の実現に向けて,平成8年度は,以下の研究を遂行した.
1.SOFLを用いて,次に述べる二つのシステムを開発するための仕様書を作成した.
・踏切制御システム・ジョージメイスン大学の入学・教育情報システム
この二つのシステムは,互いに異なる特徴を持っている.踏切制御システムは,直接,人命に係るために,絶対的な信頼性を要求される安全性が必須な(Safety Critical)システムである.それに対して,教育情報システムは情報の整合性と安全性が要求される.これらの応用事例に適用した結果に基づき,SOFL言語及び,SOFL方法論を改良し,形式手法の新しい開発方法論"形式的工学手法"を構築した.本研究に関して,以下の5編の論文を作成した.
(1)"A Model-Oriented Approach to Safety Analysis Using Fault Tress and a Support Systems"(発表した)
(2)"A Case Study Using SAM-Safety Analysis of PES"(発表した)
(3)"SOFL : A Formal Engineering Methodology for Industrial Applications",(投稿中, IEEE Transactions on Software Engineering)
(4)"A Formal Specification of Fault Tress for SAM"(投稿中,情報処理学会論文誌)
(5)"The SOFL Approach : An Improved Principle for Requirements Analysis",(投稿中,情報処理学会論文誌)
2.形式仕様からプログラムへの自動変換は,一般的には困難とされている.しかし,人が介在することにより,形式仕様からプログラムを半自動的に変換することは,十分に可能である.この実現に向けて,前置条件と後置条件を用いた仕様を,半自動的に変換する新しい理論を構築した.本理論
… More
においては,SOFL仕様をプログラムに変換する際,まず最初に,ルールを用いて抽象的なプログラムを自動的に生成する.次に,この抽象的なプログラムを手動で変換することで,具体的なプログラムを生成する.本研究について発表した論文は,カナダのモントリオールで開催されたIEEE Computer Society主催の国際会議において「優秀論文賞」を受賞した.
(6)"Semi-automatic Transfromation from Formal Specifications to Programs"(発表した)
3.既存の形式仕様の詳細化技術は,高度に複雑なシステムを構築するためには,実用上大きな困難が伴う.この問題を解決するために,新たな詳細化理論を構築した.これは,我々のソフトウェア開発方法論が有効となるための基礎になることが期待される.本研究については,以下の論文を作成した.
(7)"Evolution : A More Practical Approach than Refinement for Software Development" (投稿中, Third IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'97))
4.構造化形式手法を基にしたソフトウェアテスト技法に関する研究を通して,形式仕様のテスト及び形式仕様を基に開発されたソフトウェアのテストの両者を行うための,具体的なテスト生成のルールを作成した.この二つは,密接に関係しているが,従来のテスト生成の技法とは目的が異なる.前者は仕様の整合性を検証するため,形式仕様を実行せずに,仕様をテストする手法である.後者は,形式仕様を基に作成されたソフトウェアの正しさを保証するテスト手法である.この二つのテスト方式の研究に関しては,以下の論文を作性した.
(8)"An Approach to Testing object-Oriented Formal Specifications" (発表した)
(9)"Generating Test Data from SOFL Specifications" (投稿中, Journal of Systems and Software)
(10)"Rigorous Reviews for SOFL Specifications through Specification Testing" (準備中)
5.SOFL仕様を基にした厳密なレビュー手法とSOFLのコンパイラを構築するため,SOFLの形式的意味を研究し,基礎的な公理的意味論と操作的意味モデルを構築した.本研究に関しては,以下の論文を作成した.
(11) "A Formal Definition of FRSM and Applications", (投稿中, International Journal of Software Engineering and Knowledge Engineering)
(12) "A Formal Operational Semantics for SOFL" (投稿中, Third IEEE International Conference on Engineering Complex Computer Systems (ICECCS'97)
6.SOFLのグラフィカル・ユーザインタフェイス構築のための技術を研究し,基礎的なグラフィカル・ユーザインタフェイスのプロトタイプを開発した.本研究に関しては,以下の論文を作成した.
(13)"Formal Methods and Intelligent Software Engineering Environments" (投稿中, The 1997 Asia-Pacific Software Engineering Conference) Less
|
