形式仕様に基づく適応型ソフトウェア開発に関する研究

1998 Fiscal Year Annual Research Report

• Project/Area Number: 10139218
• Research Institution: Shizuoka University
• Principal Investigator: 水野 忠則 静岡大学, 情報学部, 教授 (80252162)
• Co-Investigator(Kenkyū-buntansha): 太田 剛 静岡大学, 情報学部, 講師 (40213730) ; 佐藤 文明 静岡大学, 情報学部, 助教授 (40273164) ; 吉田 敬一 静岡大学, 情報学部, 教授 (50091161)
• Keywords: プログラムスライス / 並列アルゴリズム / 形式仕様記述 / 静的解析 / 並列プログラム / 分散プログラム

Research Abstract

ソフトウェアは、その規模の大きさや利用期間の長さに応じて、仕様変更や機能追加が難しくなってくる。従来、このようなソフトウェアの環境への適応については、多くの研究が行なわれているが、まだ決定的な方法論は提案されていない。このような背景から、本研究では適応的なソフトウェアを開発するために必要なソフトウェア構造と、開発方法の研究を行なうものである。
まず、ソフトウェアの環境に適合しなくなった部分を切り出す方法として、並列マシンによるプログラムスライスアルゴリズムの実現と評価を行なった。特に、既存のスライス計算アルゴリズムの中でも、並列計算に適していると考えられる行列演算のみでスライス計算を行なうことができるμ関係行列を用いるアルゴリズムと、スライスの時間計算量の小さいプログラム依存グラフ(PDG)を用いるアルゴリズムを並列計算機に実装し、計算量の実測を行なった。この実験から、PDGを用いるアルゴリズムの方が比較的並列計算に適していることを実証した。
また、形式仕様に基づくプログラム生成・検証に関する研究として、仕様記述言語SDLに基づいた並列プログラムデバッグ用静的解析アルゴリズムの研究を行なった。分散並列プログラムの開発では、メッセージ交換の履歴を保存して、それに基づいてメッセージ交換を再現しデバッグする方式が提案されている。その履歴の情報量を削減するには、再現性のあるメッセージは保存の対象から削除することが必要であり、そのために静的解析が有効である。我々の方式では、特に再現性のなりメッセージを解析することが目的となるため、メッセージ交換に特化した解析方法により効率的な解析を可能とした。また、複数のグローバル状態をまとめて状態数を削減する方法と増分的な解析アルゴリズムにより、静的解析に問題となる状態爆発を回避することが可能となった。

Research Products

• [Publications] 太田剛: "プログラム変更に対処し易いプログラム依存グラフの一変種" 情報処理学会研究報告. 98-SE-121. 49-56 (1998)
• [Publications] 水野業介: "Pascal風言語に対するプログラムスライスの並列化" 情報処理学会第58回全国大会講演論文集. 5C-04 (1999)
• [Publications] 梶由仁: "分散並列デバッキングのコスト削減のための静的解析アルゴリズム" 情報処理学会マルチメディア,分散,協調とモバイルシンポジウム論文集. 98・8. 531-538 (1998)
• [Publications] 梶由仁: "仕様記述言語SDLに対する静的解析アルゴリズム" 日本ソフトウェア科学会ソフトウェア工学の基礎シンポジウム論文集. 5. 169-174 (1998)