近年、これまで個別に動作していたシステムがさまざまなレベルのネットワークを通じて相互に結ばれて協調動作するようになっている。このように複雑化したシステムに対する安全分析や障害原因診断では、推定要因とその箇所を絞り込んだ後に、絞り込んだ推定要因が本当の要因であることを検証することになる。また、システムの複雑化への対応策として、モデルベースでこうした分析・診断を行うようになってきている。

　例えば、システムのコンポーネント間の相互作用に着目した安全分析手法である「STAMP（System Theoretic Accident Model and Processes）/STPA（System Theoretic Process Analysis）」を用いて分析することにより、システム全体の障害を引き起こす推定要因を「コンポーネントCが性質Pを満たさないこと」といったように絞り込めることがある。推定された要因に対するモデルベース検証技術の1つが「形式手法」である。本稿では、形式手法について解説する。まず代表的な形式検証である「モデル検査」を解説し、続いて形式手法のバックエンドとして注目を浴びている「SAT（boolean SATisfiability）/SMT（Satisfaction Modulo Theory）ソルバ」を解説する。