モデル検査

システムの全ての状態を網羅的に探索し、仕様を満たすかどうかを自動的に検証する形式手法。時相論理（CTL、LTL）で記述された性質の成否を判定する。デッドロックの検出、安全性・活性の検証に有効だが、状態爆発が課題。

システムを有限の状態遷移モデルとして表し、到達しうるすべての状態を網羅的に調べて、満たすべき性質（デッドロックが起きないなど）が成り立つかを自動的に検証する手法。テストでは再現しにくい並行処理の不具合を見つけられ、性質が成り立たない場合はそこに至る手順を反例として示す。

集合論と述語論理に基づいて仕様を厳密に記述する形式仕様記述言語。曖昧さのない仕様を作れる。

形式仕様記述と段階的詳細化によってソフトウェアを開発する手法。VDMToolsなどの支援ツールがある。

標準として定められたプロセスや文書、手法を、対象プロジェクトの規模、複雑さ、リスク、組織文化に合わせて取捨選択・修正すること。標準をそのまま当てはめて過剰な管理や形骸化に陥ることを防ぐ。

ソフトウェアの企画から開発、運用、保守、廃棄までの作業内容と用語を体系化した指針。SLCP-JCFともいい、発注者と受注者が同じ言葉で話すための共通の物差しとなる。

ソフトウェアライフサイクルプロセスを定めた日本産業規格。ISO/IEC 12207に対応し、共通フレームの基礎になっている。

システムライフサイクルプロセスを定めた日本産業規格。ソフトウェア単体ではなく、システム全体の視点でプロセスを規定する。