このページでは，形式手法における記述・モデル化という側面について解説します．形式手法においては，「システムのある側面を抜き出し，抽象的に表現（モデル化）」します．逆に言えば不要な詳細を「捨象」します．これにより，人にとって，ツールにとって，分析や検証などの目的に適したモデルを記述していきます．ここでモデル化の方針は，手法により多かれ少なかれ異なっています．また，同じ手法，同じ記述方式を用いるにしても，開発者自身が目的を意識してモデル化の方針を定める必要があります．
ここまで形式手法・ツールの例としてSPIN，VDMをごく簡単に紹介してきました（SPINの例，VDMの例）．以下ではこれらを例として，形式手法におけるモデル化・記述という一つのポイントを説明します．
非常に大ざっぱに言ってしまうと，SPINにおいては「複数のプロセス（スレッド）においてどういった順序・分岐で実行が進む可能性があるか」に焦点を絞って記述し，「その結果実行の進行に関しどのような性質が成り立つか（成り立たないか）」を検証します．一方VDMにおいては「システムの状態がどのようなデータ構造を持ち，個々の関数・操作（メソッド）がどうそれを変化させるか」に焦点を絞って記述し，「一つ一つの関数・操作の実行は，必ず期待された状態変化を起こすか（おかしな状態に遷移させないか）」を検証します．
このような記述対象，検証対象の違いは，それぞれの手法・ツールの目的に起因しています．SPINにおいては，並行・分散システムにおいて，スレッド切り替えタイミングなど特定の実行順序・分岐でのみ発生する期待しない状況を検出することを主目的としています．一方でVDMにおいては，要求文書からプログラムを導いていく途中過程における仕様や設計といった成果物を厳密化・明確化し，テスティングやプロトタイピングを行うことを主目的としています．このようにSPINとVDMなどでは，目的，視点が大きく異なり，それに応じて記述対象や記述の抽象度を想定し，記法を定めています．
また，大まかには同じ目的，視点であったとしても，「実行の順序（AよりBが先に起きるかどうか）のみ考えるか，実行にかかる時間量（Aに1.5秒かかりBに3秒かかる）まで考えるか」といった差異もあります．これは「経過時間（や関連する要求，つまりリアルタイム制約）」という側面を考えるかどうか，という差異です．例えばSPIN（注：ツール名）ではこのリアルタイム性という側面を考えていませんが，UPPAALというツールでは考えています．VDM（注：手法名）およびその支援ツールにおいてはこれまでリアルタイム性という側面を想定していませんでしたが，近年その側面を扱うツールも別途リリースされています．リアルタイム性に限らず，様々な側面・詳細に関して「その側面・詳細を考慮に入れるか，省いてしまうか」という選択肢があります．
なお，実装コードから注目する部分（例えばメモリ管理処理のみ）抜き出し，検証を行うような手法・ツールもあります．そのような場合には「記述」ではなく「抽出」となりますが，同様にどのような側面・詳細を考えるかという選択肢があります．
上記のように，形式手法では最終的に動作させるシステムそのもの（実装としてのプログラム）を記述するわけではないので，「何のために，システムのどの側面をどのような抽象度で（言い換えるとどこまで詳細に）記述するのか」ということが重要になっています．逆に言うと，人にとっての見やすさや理解のしやすさ，ツールにとっての解析・検証のしやすさのため，「必要のない側面，必要のない詳細は記述しない（捨象する）」ということになります．
この考え方は，「モデル」「モデル化（モデリング）」という言葉によって説明できます．例えばOxfordの英英辞典（Concise版）には，以下のようにモデルという言葉が説明されています（残念ながら広辞苑にはこの意味は載っていませんでした）．
a simplified description, especially a mathematical one, of a system or process, to assist calculations and predictions
自然科学においてはこの定義であるように「計算」や「予測」を考えるのかもしれませんが，形式手法の場合「プロトタイピング」「分析」「可視化」「検証」といった目的のために，システムの単純化（抽象化）した表現を用いることになります．上の定義では「特に数学的な表現」とありますが，まさに形式手法の特徴は，数学的な理論に基づいたシステムのモデル化・記述を考えるところにあります．
ここまで，手法・ツールの目的に応じて，「システムのどのような側面をどのような抽象度で記述するか」というモデル化の方針が異なることを述べてきました．実際には，ある手法・記法の許す範囲で具体的な方針を定めるのは，手法・ツールを用いる開発者になってきます．開発者は以下のような要件を検討し，（手法・ツールの選択および）モデル化の方針決定を行う必要があります．
モデル化の方針の選択・決定は，多くの場合絶対的な基準があるわけではなく，難しい問題です．一般的な考え方の指針はまとめられていますが，開発者が対象システム開発における問題や要求を基に判断をする必要があります．このため，「モデル化」は形式手法の適用における「肝」となると考えられています．
例えば，SPINに関し様々な書籍が出版されていますが，どの書籍を見ても「抽象化」という章があります．これはSPINの場合，「網羅的な検証を可能とするくらい抽象的にしつつ，意味のある検証となるよう実際のシステムの重要な側面を反映する」というモデル構築が求められるからです．
またVDMにおいても，代表的な書籍が「ソフトウェア開発のモデル化技法」と名付けられているなど，モデル化は肝になると考えられています．VDMの場合，実際のプログラムに近い記法も提供しているため，何も考えずに書くと「プログラムのようなもの」も書けてしまいます．そうすると，何のためにVDMを用いているのか（プログラムとは別に仕様や設計を厳密に記述しているのか）がわからなくなってしまいます．このため，VDM適用の目的を明確にし，「システムの側面に焦点を絞ったり抽象的な記法を用いたりして，プログラムへつなぐ抽象的な（詳細は省いた）モデルを構築する」という意識を持つ必要があります．