(日本語) [学士論文] 分散ストリーム処理エンジンを用いたMTLによる大規模トレース検査

Sorry, this entry is only available in Japanese.

小林研B4の有松さんが学士論文を提出しました.

題目:分散ストリーム処理エンジンを用いたMTLによる大規模トレース検査
内容梗概:

実行トレースの検査は潜在的なバグの検出やテストにおいて有益な手法である. 一方で, プログラムの大規模化や複雑化によって, 検査対象となる実行トレースは大規模となり, 検査には膨大な時間が必要になった.

従来の研究では, 実行トレースのオフライン検査において並列化を駆使して検査時間を減らす手法や, 実行トレースを用いることなくオンライン検査を行うという手法が存在する. しかし, オフライン検査では大規模な実行トレースを記録した巨大なファイルを保存しなくてはならない. また, 従来のオンライン検査の手法では事前に監視対象のプログラムを加工する必要があり, 実行中に監視対象を変更することができない.

また一方で, 実行トレースの検査においてはイベントの相互関係の表現が重要になる. これを表現する手法として時相論理が存在するが, 古典的な時相論理では定性的な時間の関係しか扱えず不十分である.

本研究では, 分散ストリーム処理エンジンとMTL(Metric Temporal Logic)を用いてオンライン検査する処理基盤を実現した.

分散ストリーム処理エンジンにより, 監視対象のプログラムを加工しないで効率的に実行トレースをオンライン検査できる. また, オンライン検査のため, 実行トレースをファイルに記録する必要がない.
加えて, MTLを導入することにより, 定量的な時間を用いたイベントの相互関係の表現ができる.

また, その実装したツールを用いて実験を行った. その結果, 10のイベントが関連するMTL式の検査では1ミリ秒当たり5,892のイベントが処理でき, かつMTLの一つの部分式の判定は30マイクロ秒程度で行うことができ, 実用上十分な性能であることを確認できた.