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

1997 Fiscal Year Annual Research Report

• Project/Area Number: 09245214
• Research Institution: Shizuoka University
• Principal Investigator: 富樫 敦 静岡大学, 情報学部, 教授 (20172140)
• Co-Investigator(Kenkyū-buntansha): 白鳥 則郎 東北大学, 電気通信研究所, 教授 (60111316) ; 西垣 正勝 静岡大学, 情報学部, 助手 (20283335)
• Keywords: 発展可能 / ソフトウェア開発 / 要求記述 / 使仕様記述 / 要求診断システム / 検証システム / 開発支援環境 / プロトタイピング

Research Abstract

本研究では,簡単化のため第2階様相述語論理に基づいた発展可能ソフトウェアの新しい要求記述法と,その状態遷移システムによる形式仕様の自動生成に関する基礎理論を発展しつつあり,現在そのための支援システムを開発中である.具体的には,システム要求記述を機能の局所的な性質を記述した理論式として定式化する.また,システム要求の意味は健全でかつ完全な遷移システム(標準モデル)であるという意味論を提案し,その妥当性を理論的かつ実際的側面から議論した.この標準モデルがシステムの形式仕様であり,システム要求の実現である.この意味論は,論理ペトリネットを用いても特性化できることを示した.これは,研究項目(2)と密接に関連する.さらに,複雑な大規模システムの要求記述と仕様化に対処するため,制約によるモジュール化技法,論理ベースの抽象化と階層的詳細化などを研究し,状態爆発と複雑さの問題を部分的に解決した.以上の基礎研究を踏まえ,システム要求記述言語を設計し,システム要求の意味でありかつそれ自身がシステムの形式仕様である「状態遷移システム」を効率よく生成するための理論と実際の導出法を与えた.
命題理論に基づいた記述法については既に研究成果を得ていたが,実用性と適用制の範囲を考慮すると,命題論理は余りにも記述能力が低い,しかし,単純に第2階の様相理論に拡張したのでは,計算可能性や高率の点で問題が生じる.そこで,本研究では,一挙に第2階様相述語論理までレベルアップしたことによる問題の他,発展可能なソフトウェアの要求記述,仕様化に柔軟に対処するため,以下の点を考慮した要求記述法並びに記述言語の設計とその意味論に基づいた状態遷移システムベースの形式仕様に変換する手法を与え,ワークステーション上にSICtus Prologを用いて仕様合成システムを開発している.

Research Products

• [Publications] A.Togashi, F.Kanazashi, X.Lu: "A methodology for the description of system requirements and the derivation of formal specifications" proc.of FORTE/PSTV97. 125-142 (1997)
• [Publications] 金指文明, 富樫敦: "π計算に対する証明システム" ソフトウェア光学の基礎IV,FOSE'97ワークショップ論文集,近代科学者社. 20-27 (1997)
• [Publications] 金指文明, 陸暁松, 富樫敦: "ソフトウェアの効果的な開発環境" ソフトウェア工学の基礎IV,FOSE'97ワークショップ論文集,近代科学社. 67-70 (1997)
• [Publications] 陸暁松, 金指文明, 富樫敦: "システム要求と仕様記述の診断" ソフトウェア工学の基礎IV,FOSE'97ワークショップ論文集,近代科学社. 39-42 (1997)
• [Publications] A.Togashi: "On Typing Systems for the Polyadic pi-Calculus" Proc.of RIMS Workshop in Computing titled Concurrency Theory and Applications'96. 125-142 (1997)
• [Publications] A.Togashi: "Name matching v.s. structure matching in typing systems for the polyadic π-calculus" 静岡大学情報学研究. 1. 25-42 (1997)