機器の高速化やネットワークの発展に伴い，多数の機器やコンポーネントを連携させ，高度な機能を提供する並行分散システムが一般的になってきている．そのようなシステムでは，振舞いの可能性が膨大であり，従来のレビューやシミュレーションで設計の振舞いの正しさを保証することは困難である．それに対して，網羅的にかつ自動的に振舞いに関する性質を調べるモデル検査技術が注目されている．本稿では，モデル検査技術の背景と5つの代表的なモデル検査ツールを紹介し，その応用事例や最新の研究動向を解説する．