「VDM」の版間の差分

履歴の双方向閲覧

← 古い編集新しい編集 →

削除された内容追加された内容

ビジュアルウィキテキスト

インライン

2007年6月25日 (月) 07:05時点における版

VDM（Vienna Development Method）は、IBMのウィーン研究所で1960年代から70年代にかけて開発された形式手法。

その仕様記述言語VDM-SLは1996年にISO標準（ISO_IEC_13817-1）となっている。VDM-SLをオブジェクト指向拡張したVDM++も、欧州連合ESPRIT計画のAFRODITEプロジェクトで開発された。

この項目は、書きかけの項目です。この項目を加筆・訂正などしてくださる協力者を求めています。

このテンプレートは分野別のスタブテンプレート（Wikipedia:スタブカテゴリ参照）に変更することが望まれています。

@@ 7行目: / 7行目: @@
 [[en:Vienna_Development_Method]]
 [[uk:Віденський_метод_розробки]]
-形式手法とは、1970年代から始められたプログラム開発手法の1つで、論理学や離散数学などが基礎になっています。プログラムの正しさに関する数学的な証明体系として整理された理論をベースとし、形式仕様記述やモデル検査へと研究対象を発展させてきています。最初は取りあえず、「品質向上のための手法（ツール）」ととらえてもよいでしょう。
-■CSKシステムズは，フォーマル・メソッド（formal methods）の一種である「VDM」の普及や認知を目的とした「VDM研究会」を設立した（CSKシステムズによる設立趣意）。VDMとは，「VDM++」や「VDM-SL」など仕様を記述することに特化した専用言語でシステムの仕様を詳細に書き出すことで，仕様の矛盾や不整合などのバグを洗い出すための方法論である。VDM研究会は，コンサルティング会社，VDMの活用企業，大学教授などで構成する。
-　VDM（Vienna Development Method）は，1970年代にオーストリアIBM Vienna研究所で開発されたフォーマル・メソッドの一手法である。コンパイラの仕様検証を目的に開発された。「ISO/IEC 13817-1」として規格化されている「VDM-SL」やオブジェクト指向に対応した「VDM++」といった形式的仕様記述言語を用いて，ソフトウエアの詳細仕様を記述する。
-　一般に，ソフトウエアの仕様は日本語などの自然言語やUMLなどで記述されることが多い。状態遷移図やフロー・チャートなどで補足することはあるものの，プログラムの実装者やテスト担当者がいざ仕様書を読むと，曖昧な点や行間を読まないと理解できない側面も多い。VDM++やVDM-SLには，事前条件や事後条件など，ある操作の仕様を明確に記述するための構文などがあらかじめ用意されているため，仕様の策定者自身がより詳細な仕様を突き詰め，厳密に表現しやすいという特徴がある。
-　フォーマル・メソッドは発祥地である欧州では認知・普及も進んでいるが，日本国内では適用事例は少ない。CSKの子会社だった日本フィッツ（現在は，CSKシステムズに統合）が証券システムの開発で利用したり，フェリカネットワークスが携帯電話機向けの非接触IC「モバイルFeliCa」の次世代版の開発においてファームウエアの仕様検証に使ったりした程度である。フェリカネットワークスでのVDM適用では，日本フィッツが支援した。
-　CSKシステムズは，こうした日本フィッツやフェリカネットワークスでのVDMの適用経験を生かし，主に組み込みソフトウエア開発などに向けてVDMの認知・普及を進めたい考えである。今回のVDM研究会の会員は比較的少数だが，将来的にはより会員のすそ野を広げた「VDMコンソーシアム」を発足させる計画という。
-◆VDMToolsの最新版も発表
-　VDMそのものは方法論や言語であるため，利用に当たって特に専用のツールは必須ではないが，「VDMTools」という開発支援ツールも存在している。デンマークのベンチャー企業であるIFAD社が開発したもので，CSKシステムズは2005年にVDMToolsの知的資産をIFAD社から買収している。現在，同ツールの組み込み分野向けの改善や保守，サポートなどもCSKシステムズが手掛けている。2006年3月7日には，メニューを日本語化するなどした最新版を同社が公開した。
-　なお，日経エレクトロニクスは2005年12月19日号の特集記事「ソフトウエアは硬い」において，フォーマル・メソッドについて詳報しております。フェリカネットワークスにおけるVDM適用事例のほか，モデル検査などフォーマル・メソッド全般の動向について解説しています（関連記事）。また，2006年4月19日には，フォーマル・メソッドの一種である「モデル検査」に関するセミナーを開催します（詳細はこちら）。こちらもぜひご参加下さい。
-■形式手法は、システムの大規模化・複雑化から、上流工程での品質改善手段として最近日本でも注目を集めるようになりました。また、海外では規格・標準において形式手法を推奨もしくは必須とするものが現れ、日本企業も真剣に取り組まざるを得ない状況になってきました。
-　形式手法には多種多様な側面があります。本稿では、形式手法の最も重要な要素である仕様を厳密に記述することを主目的にする仕様記述部分モデルを検証することを主目的にする形式検証部分を簡単に紹介した後、仕様記述部分である形式仕様記述について説明します。
-■形式仕様記述（形式的仕様記述）
-　「形式仕様記述」は、仕様の厳密な定義を目的としています。
-　システムが「仕様」として定義され、これが開発のベースとなる現在の開発スタイルにおいて、仕様作成者の意図を正しくシステムに反映させるには、仕様作成者がシステムを直接開発・検証するか、正しい仕様と対比してシステムを開発・検証する必要があります。しかし、仮に仕様作成者がすべての開発・検証を行ったとしても、仕様自体に矛盾や未定義事項があれば、システムが正しく振る舞うことを保証できません。
-　そこで、矛盾がなく論理的に正しい仕様を作成するために考案されたのが形式仕様記述です。形式仕様記述を行うための「仕様記述言語」には、VDM-SL、VDM++、RAISE/RSL、Z、B、Clear、OBJ、CafeOBJ、CASL、LOTOSなどがあります（注）。
-注：VDM-SLは1996年に、Zは2002年にISOにて標準化されています。
-　主な仕様記述言語の1つである「VDM-SL（Vienna Development Method - Specification Language）」は、もともとプログラミング言語の研究であるウィーン定義言語（Vienna Definition Language）の流れをくみ、欧州では現在まで40年以上も研究・実用が継続されています。日本ではようやく大規模な事例が出てきたという段階であり、かなり後れを取っています。
-※形式手法の必要性とメリット
-　形式手法が古くから研究されてきた分野であると前述しましたが、なぜいまになって取り上げられているのでしょうか。
-　海外では長い間、人工衛星や航空機、原子炉の制御といったミッションクリティカルなシステムにおいて形式手法が利用されてきました。もちろん今後も形式手法は欠かせない技術です。
-■自然言語におけるあいまいさ
-　さて、皆さんはどのような仕様書を作成しているのでしょうか。CDプレーヤのディスク取り出し機能を例に、少し考えてみましょう。
-　まず、「CDのEJECTボタンが押されたらCDを排出する」という仕様を書き、次に「再生中の場合は停止して」「停止中の場合は……」などと書いてだんだん条件が複雑化。文章だけでは分かりにくくなったので表を添付する、という感じでしょうか。ここまで書いて次は設計です。UMLで状態遷移図とシーケンス図を描いて、いよいよ実装に入ります。
-　プログラマーは、「再生中とは何か」「シーク中は再生中か」を考えます。優秀なエンジニアは条件をまとめて仕様作成者とコミットするでしょう。人によってはそのような状態を考えずに実装します。結果として、製品の仕様に作成者たちも分からない状態ができてしまいます。私はいままでそういう現場を見てきました。
-　では、形式手法ではない方法、つまり自然言語では厳密な仕様は記述できないのかというと、不可能ではないと思います。ただし、自然言語ではどのような記述も許されてしまい、一意に解釈できる記述を行うのは困難です。仮に自然言語で厳密な仕様を記述できたとしても、理解しにくい冗長な表現になってしまうでしょう。また、ルールのない記法において、仕様が正しいことを証明する手段はありません。
-　自然言語で仕様を記述した場合、仕様自体にあいまいさが入り込む可能性が高く、第三者が開発・検証を行ったり、検証を自動化するのは困難です。形式仕様記述では数学的な表記ができるよう記法が定義されており、論理的な記述により事象を明確に定義することができます。
 [[Category:形式手法]]