メッセージ・シークエンスーチャートに対するSATソルバーを用いたディスコード計算手法

摘要

Message Sequence Chart is a method for representing interactions between concurrent processes visually, which has been incorporated to UML. On the other hand, only minimum orders among events are specified in the charts, which is one of the main features, may lead to unintentional descriptions where event orders are not what the users wish to describe. In order to analyse such situations, Peled et.al proposed a concept of "discord" and an algorithm for computing discords for a message sequence chart. Their algorithm, however, requires exponential computational time in terms of the size of the given message sequence chart. In this report, we show a new SAT-base algorithm for discord computation.%メッセージ・シークエンス・チャートは並行プロセス間の動作を図的に表現する手段として提案され，UMLなどにも取り込まれる形で利用が進んでいる．一方，イベント間の発生順序を必要最低限しか指定しないという特性をもつため，ユーザがかならずしも意図しないイベント発生系列を含む場合がある．これを解析するための手段として，ディスコードの概念がPeledらによって提案され，計算アルゴリズムが示されているが，与えられたメッセージ・シークエンス・チャートのサイズに対して，指数的な計算時間を要する．本報告では，SATを使ったディスコード計算のアルゴリズムを示す．