氏名: 平手 孝 (289634377)
論文題目: 通信プロセスのテスト等価性検証のための視覚的支援環境
論文概要
通信プロセスをモデルとする並行プログラミングでは、外部的な振舞いを
仕様として表し、サブプロセスを合成して実現する。
この実現プロセスが、仕様で定められる動作を満たすように修正を加える
過程をデバッグとする。
しかし、通信プロセスでは非決定的な動作および通信のメカニズムのため
に、このようなデバッグは一般に難しい。
この問題に対し、通信プロセスの動作モデルであるラベル付遷移システム
を直接視覚的に表現することにより、通信プロセスモデルにおける
デバッグを支援する環境を提案する。
ユーザーは、まず仕様と実現を表すラベル付遷移システムをデバッガに
与える。
デバッガは、それらをDeNicola Hennessy のテスト意味論の十分抽象的な
モデルである受理グラフに変換し、実現の受理グラフを仕様の受理グラフ
と等価になるようにデバッグを行う。
仕様と実現が等価になった場合、デバッグは終了する。
受理グラフの等価性検証は、Cleavelandらの診断テスト生成のアルゴリズ
ムを拡張して用いた。
このアルゴリズムで生成された診断テストプロセスにより、
2つの受理グラフの相違点を見つける。
ユーザーは、同定された実現プロセスの状態を修正する。
さらに本支援環境は2つのグラフを等価にする具体的な修正方法を
視覚的なインターフェースを通じて提案する。
実現プロセスが、単一プロセスの場合には上記のデバッギング手法が
そのまま適用でき、プロセス全体への修正は直接的に行われる。
しかし、実現プロセスは一般にサブプロセスの並行合成で構成されている。
本支援環境ではサブプロセスの組み合わせに対する相違点の同定お
よび修正方法をサブプロセス毎に展開して提示できるようにデバッギング
手法を拡張し、支援環境を構築した。
目次に戻る