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

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

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