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

Sorry, this entry is only available in Japanese.

小林研 B4の有松優さん,D3の野田釧広さん,小林准教授が、沖縄県の那覇で開催されたIEICE ソフトウェアサイエンス研究会 3月研究会にて、有松さんの学士論文の成果をもとにした研究発表を行いました。分散ストリーム処理エンジンを用いて時相論理(Metric Temporal Logic)で記述された制約をオンライン検査する手法を提案しています。

著者: 有松優・野田訓広・小林隆志(東工大)
題目: 分散ストリーム処理エンジンを用いたMTLによる大規模トレース検査
掲載誌: 信学技報, vol. 118, no. 471, SS2018-73, pp. 127-132, 2019年3月
概要:
システムが満たすべき制約を時相論理等により表現し,実行トレースに対して制約の成立有無を検査することで,潜在的な不具合の検出を行うことができる.
実行トレースは膨大な規模となるため,検査の効率化が重要であり,これまでに,実行トレースのオフライン検査を並列化することで検査時間を短縮する手法が提案されている.
しかし,膨大なトレースデータの記録のため多大な記憶領域が必要となることに加え,トレース全体の検査には依然として膨大なリソース・計算時間を要してしまう.

本研究では,大規模な実行トレースに対し,分散ストリーム処理エンジンを用いて,MTL (Metric Temporal Logic)で記述された制約のオンライン検査を行う手法を提案する.
提案手法では,対象のシステムを停止させることなく,実行トレースをストリームデータとして取得し,オンラインに制約検査を行う.
膨大なトレースデータを保存する必要がなくなり,対象システムの実行と同時に制約検査ができるため,オフライン検査に比べて実質的な検査時間を大幅に低減できる.
実験により,提案手法が,実用上十分な性能で,制約をオンライン検査できることを示す.