1998 Fiscal Year Annual Research Report

発展可能ソフトウェアの開発法に関する基礎と支援環境の構築

Research Project

Project/Area Number	10139216
Research Institution	Shizuoka University
Principal Investigator	富樫敦静岡大学, 情報学部, 教授 (20172140)
Keywords	発展可能 / ソフトウェア開発 / 要求記述 / 仕様記述 / 要求珍断システム / 検証システム / 開発支援環境 / プロトタイピング
Research Abstract	(1) 発展可能ソフトウエアの要求記述法と形式仕様の自動生成法に関する継続研究平成9年度では,命題論理に基づいた新しい要求記述法と,その状態遷移システムによる形式仕様の自動生成に関する基礎理論を展開し,その処理系を開発した.しかし,実用性や適用範囲の広さを考慮すると,命題論理では余りにも記述能力が低い.しかしながら,単純に第一階述語論理や高階(様相)論理に拡張したのでは,計算可能性や効率の点で問題が生じる.そこで,本年度は,平成9年度の研究成果である要求記述法や処理系を拡張し,制限された第二階様相論理に基づいた要求記述法と記述言語の設計ならびにその処理系をjavaを用いて分散環境上に実現した.研究開発に当たり考慮した点は以下の通りである. (a) 機能の記述は述語論理の範囲で行なった,制約の記述を第二階様相論理で行なった.ただし,命題論理の場合と同じような意味論が第二階様相述語論理に拡張しても展開でき,要求記述のモデルである形式仕様への変換が効率的に行なえること.その際問題になる効率や状態の爆発を,述語によるラベル機能を用いて克服した. (b) 大域的制約,局所的制約を用いたモジュール化技法.抽象化と階層的詳細化の導入. (c) 要求の変化に柔軟に対処可能なやわらかい要求記述法と仕様化技術の達成. (d) 状態遷移と状態の機能に対する外延的性質による新しい等価性の理論の確立. (2) 発展可能ソフトウェアシステム要求診断・検証システムの基本設計曖昧で不完全な要求記述を対象とし,その意味である状態遷移システムのユーザの解釈に基づき,正しくない状態遷移,抜けている状態遷移,矛盾した意味を持つ状態などの診断項目により,要求記述を診断するシステムの基本設計を行なった.また,要求記述の時間に関する動的かつ大域的な性質を検証するための時制論理による検証システムの基本設計を行なった.両システムの実装は,平成11年度に行なう.

Research Products
(12 results)

All Other

All Publications (12 results)

[Publications] 石井基樹, 山田将弘, 金指文明, 陸暁松, 富樫敦: "リアクティブシステム開発のための統合型支援環境" ソフトウェア工学の基礎IV,レクチャーノート/ソフトウェア工学20,日本ソフトウェア科学会FOSE'98,近代科学社. 50-55 (1998)
[Publications] 金指文明, 陸暁松, 富樫敦: "形式仕様からシステム要求への反映" ソフトウェア工学の基礎IV,レクチャーノート/ソフトウェア工学20,日本ソフトウェア科学会FOSE'98,近代科学社. 74-79 (1998)
[Publications] 金指文明, 陸暁松, 富樫敦: "システム要求からの形式仕様の導出方法" 情報処理学会論文誌. Vol.40,No.1. 310-321 (1999)
[Publications] Xiaosong Lu, Fumiaki Kanezashi, Atsushi Togashi: "Hierarchical Specification of Reactive System Requirements" Proc.of the 13th International Conference on Information Networking(ICOIN-13). 10B. 10B-3.1-10B-3.6 (1999)
[Publications] Atsushi Togashi, Fumiaki Kanezashi: "A Modal Proof System for Mobile Processes" 情報処理学会研究報告. 98-MBL-6. 67-74 (1998)
[Publications] 金指文明、塚崎悟、富樫敦: "π計算に対する視覚化システム" 情報処理プログラミング研究会. (1998)
[Publications] 塚崎悟、金指文明、富樫敦: "π計算に対する動作視覚化システム" 情報処理学会第57回全国大会. 1E-4. (1998)
[Publications] 金指文明、富樫敦: "π計算に対する様相証明システム" 情報処理プログラミング研究会. (1998)
[Publications] 金指文明、陸暁松、富樫敦: "システム要求記述と形式仕様の導出-デバッグ結果の反映方法-" 情報処理プログラミング研究会. (1998)
[Publications] 山田、石井、金指、富樫: "システム要求仕様化のための状態遷移システム表示インターフェースの開発" 情報処理学会第57回全国大会. 1E-4. (1998)
[Publications] 石井基樹、山田将弘、金指文明、富樫敦: "効果的なソフトウェア開発のためのシステムシミュレ一タ" 情報処理学会第57回全国大会. 1E-4. (1998)
[Publications] 富樫敦: "オートマトンと形式言語,電子情報通信ハンドブック" 電子情報通信学会編,オーム社, 6 (1998)

1998 Fiscal Year Annual Research Report

発展可能ソフトウェアの開発法に関する基礎と支援環境の構築

Principal Investigator

富樫 敦 静岡大学, 情報学部, 教授 (20172140)

Research Products

[Publications] 金指文明, 陸暁松, 富樫敦: "形式仕様からシステム要求への反映" ソフトウェア工学の基礎IV,レクチャーノート/ソフトウェア工学20,日本ソフトウェア科学会FOSE'98,近代科学社. 74-79 (1998)

[Publications] 金指文明, 陸暁松, 富樫敦: "システム要求からの形式仕様の導出方法" 情報処理学会論文誌. Vol.40,No.1. 310-321 (1999)

[Publications] Xiaosong Lu, Fumiaki Kanezashi, Atsushi Togashi: "Hierarchical Specification of Reactive System Requirements" Proc.of the 13th International Conference on Information Networking(ICOIN-13). 10B. 10B-3.1-10B-3.6 (1999)

[Publications] Atsushi Togashi, Fumiaki Kanezashi: "A Modal Proof System for Mobile Processes" 情報処理学会研究報告. 98-MBL-6. 67-74 (1998)

[Publications] 金指文明、塚崎悟、富樫敦: "π計算に対する視覚化システム" 情報処理プログラミング研究会. (1998)

[Publications] 塚崎悟、金指文明、富樫敦: "π計算に対する動作視覚化システム" 情報処理学会第57回全国大会. 1E-4. (1998)

[Publications] 金指文明、富樫敦: "π計算に対する様相証明システム" 情報処理プログラミング研究会. (1998)

[Publications] 金指文明、陸暁松、富樫敦: "システム要求記述と形式仕様の導出-デバッグ結果の反映方法-" 情報処理プログラミング研究会. (1998)

[Publications] 山田、石井、金指、富樫: "システム要求仕様化のための状態遷移システム表示インターフェースの開発" 情報処理学会第57回全国大会. 1E-4. (1998)

[Publications] 石井基樹、山田将弘、金指文明、富樫敦: "効果的なソフトウェア開発のためのシステムシミュレ一タ" 情報処理学会第57回全国大会. 1E-4. (1998)

[Publications] 富樫敦: "オートマトンと形式言語,電子情報通信ハンドブック" 電子情報通信学会編,オーム社, 6 (1998)

富樫敦静岡大学, 情報学部, 教授 (20172140)