形式手法のポイント（１）： モデル化・記述｜ディペンダブル・システムのための形式手法の実践ポータルこのページでは，形式手法における記述・モデル化という側面について解説します．形式手法においては，「システムのある側面を抜き出し，抽象的に表現（モデル化）」します．逆に言えば不要な詳細を「捨象」します．これにより，人にとって，ツールにとって，分析や検証などの目的に適したモデルを記述していきます．ここでモデル化の方針は，手法により多かれ少なかれ異なっています．また，同じ手法，同じ記述方式を用いるにしても，開発者自身が目的を意識してモデル化の方針を定める必要があります． ここまで形式手法・ツールの例としてSPIN，VDMをごく簡単に紹介してきました（SPINの例，VDMの例）．以下ではこれらを例として，形式手法におけるモデル化・記述という一つのポイントを説明します． システムのどの側面を形式化，記述し，どのような性質を検証するか？ 非常に大ざっぱに言ってしまうと，SPINにおいては「複数のプロセ
