「VDM」の版間の差分

2,707 バイト追加 、 14 年前
編集の要約なし
形式手法とは、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コンソーシアム」を発足させる計画という。
 
 形式手法は、システムの大規模化・複雑化から、上流工程での品質改善手段として最近日本でも注目を集めるようになりました。また、海外では規格・標準において形式手法を推奨もしくは必須とするものが現れ、日本企業も真剣に取り組まざるを得ない状況になってきました。
 形式手法には多種多様な側面があります。本稿では、形式手法の最も重要な要素である仕様を厳密に記述することを主目的にする仕様記述部分モデルを検証することを主目的にする形式検証部分を簡単に紹介した後、仕様記述部分である形式仕様記述について説明します。
 
匿名利用者