LMNtalモデル検査器における状態爆発対策

摘要

システム検証技術として注目を集めるモデル検査は，必要なメモリと時間が爆発的に増加（状態爆発）する問題を抱えており，大規模な検証問題を解くためには状態爆発対策の導入が必要不可欠である．LMNtalモデル検査器では，状態をバイト列へ圧縮して管理する機能を新たに導入したことで検証可能な問題の規模が拡大し，検証の長時間化への対策が求められていた．本論文では，LMNtalモデル検査器がこれまで扱うことが困難であった大規模な検証問題を高速に解くために導入した共有メモリ環境下における並列処理機能の実装と，性能評価を示す．%Model checking is an important technique for system verification based on exhaustive search, but large-scale model checking must address the inherent problem of state-space explosion both in terms of time and memory usage. The LMNtal model checker, based on the hierarchical graph rewriting model, has recently been improved by introducing state compression using binary strings. This enabled us to verify larger problems, which made it apparent that the verification must be speeded up by parallel processing. In this paper, we show the implementation techniques of our parallel LMNtal model checker for shared-memory multiprocessors, and evaluates its performance, checking using LMNtal. checker on shared-memory multiprocessors for an approach to time exlosion while doing the state compression technique by encording to binary strings for an approach to space exlposion.