Web教材一覧システムの調達

VDMの概要


VDMとは

システム開発において、論理的に正確な仕様を作成すること、それが正しいことを検証することが重要なのは言うまでもありません。仕様を記述し、その仕様を検証する手法の一つにVDM(Vienna Development Method)があります。
 VDMは、仕様を記述することに特化した手法ですから、要求分析工程に強力な手法です。しかし、表現力が高く参照にも優れているので、設計工程でも使えます。

VDMは形式手法の発端ともいわれ、1970代にIBMのウィーン研究所にてPL/Iコンパイラの正しさを検証するために開発されたものです。かなり歴史のある手法ですが、近年、発展が進んでいます。

DFDやUMLなどの図式表現で記述した仕様では、あいまいさや解釈の違いを完全になくすことはできず、人間による説明が不可欠です。それに対して、形式手法(Formal Methods)とは、数学的な集合論や論理学の考え方を基にした記述法なので、システムやソフトウェアの仕様を(少なくとも論理的には)正確かつ詳細に記述できます。また、そのような記述形式ならば、正しさを検証する(矛盾や不備を見つける)ことも容易になります。
 しかし、形式手法を駆使するのは専門的知識が必要になります。その対処として、VDMでは「記述力」と「検証力」のバランスを考慮した記述方法を採用しています。

VDMの記述言語

VDMは、次の3つの仕様記述言語を持っています。