モデル検査による設計検証

摘要

As performance of devices Decome high and growing networks between the devices, parallel and distributed systems providing advanced features become popular. It is hard to verify the behavior of such systems' design with traditional techniques, such as manual reviews and simulations, because of so many possibilities of the behavior. Model Checking is the one of promising techniques to tackle the difficulty. In this paper, we introduce the background of Model Checking techniques and show five popular model checking tools with the case studies and current research topics.%機器の高速化やネットワークの発展に伴い，多数の機器やコンポーネントを連携させ.高度な機能を提供する並行分散システムが一般的になってきている.そのようなシステムでは.振舞いの可能性が膨大であり.従来のビューやシミュレーションで設計の振舞いの正しさを保証することは困難である.それに対して，網羅的にかつ自動的に振舞いに関する性質を調べるモデル検査技術が注目されている.本稿では，モデル検査技術の背景と5つの代表的なモデル検査ツールを紹介し，その応用事例や最新の研究動向を解説する.