河原崎裕朗
サービス競合検出効率化手法
Abstract:本稿は，サービス競合検出手法の効率化手法についてまとめたものである．
ATRでは，通信サービス仕様をFSMとして表現し，それに対して到達可能性解析を行い，その結果を用いてサービス競合を検出する手法（非決定性・異常な状態への遷移）を提案している．しかし，到達可能性解析には状態爆発（解析を行うために必要となる時間や記憶容量が指数関数で増加する）という問題がある．
本稿は，ペトリネットの静的解析の結果得られるT-インバリアント（ある状態からその状態に遷移するまでの各遷移の遷移回数のベクトル）を用いて遷移の上限を設定することにより，状態爆発を回避する手法について述べる．
サービス競合の分類としては提案されていても，具体的な検出手法の提案が行われていない，異常な遷移．遷移の消失・状態の消失に関しても，T-インバリアントを用いた効率的な検出手法を提案する．