オランダ花市場 - 個別事例分析結果 - はじめに独立行政法人情報処理推進機構技術本部ソフトウェアエンジニアリングセンター ( 以降 IPA/SEC と略す ) では仕様書作成に形式

4. 個別事例分析結果

客レビューを効果的に実施することができた。

本プロジェクトは既存システムへの拡張だが、拡張部分は既存システムとネットワーク越しに接続されるものであり、また、いわゆる e-commerce としての要求は既存システムにはないものであったことから、拡張部分も新規開発と同様に要求定義から仕様記述を経て実装、テストが行われた。

要求はオークション主催者とのインタビューで獲得され、UML のユースケース、コラボレーション図、クラス図としてまとめられ、それに対応する形で VDM++仕様が記述され

た。UML と VDM++仕様は相互に繰り返し改良が行われていった。また、既存システムお

よびそのインタフェース仕様はそれまで既存システムの維持管理をしていた技術者チームが持っており、その仕様をベースに拡張部分のインタフェースに関する VDM++仕様が定義された。

VDM++で記述された仕様は、オークション主催者の技術者チームにより C++で実装され

た。テストは既存システムの動作を模擬するシミュレータによって行われた。テストにおいて新規開発部分だけでなく、既存システム側のインタフェース仕様の更新漏れが発見された。

開発プロセスをデータフローダイアグラムとして記述したものを下図に示す。

図4-16: 開発プロセス概要[HS11]

このプロジェクトで形式手法に関連して用いられた主な言語と主なツールを以下に挙げる。

表4-18: 形式手法に関して利用された言語と主なツール

UML VDM++

ファイル形式 Rational Rose LaTeX

構文/型検査 Rational Roseによる

作図

VDMTools

静的検証(証明等) -

動的検証(テスト等) - VDMTools

自動生成 - VDMToolsとRational Roseの連携機能

(1) 顧客のコミットメント

UML および VDM++で記述された仕様を繰り返し改善しレビューを行うことで、オーク

ション運営側からの十分なコミットメントを受けることができた。

(2) 十分なテスト

VDM++による厳密な仕様とそこからくるテストケースにより、良質なテストが可能になった。その結果、既存システムのインタフェース仕様と実際の動作に違いがあることも発見された。

(1) 形式手法のツールと他のツールの連携

UMLツールであるRational Roseと形式手法のツールであるVDMToolsを連携させることで、UML による要求獲得と VDM++による仕様記述を連携させることができ、繰り返し改善による仕様記述の質の向上と顧客レビューを通しての顧客のコミットメントにつながった。

原始要求を提供するオークション主催者とは UML を使ったコミュニケーションが行われた。UML と VDM が相互に派生し合い、繰り返し改良を行った結果をオークション主催者がレビューすることで、オークション主催者側のコミットメントが得られた。

下流工程を遂行したオークション主催者の技術者チームは、UML と VDM 両方の記述を参照し、C++による実装を行った。UML の各図を理解する上で、ツール連携を通して VDM++の記述を参照できることが非常に役に立った。

オークション主催者の技術者チームは VDM++についてクラスルーム形式による教育を受けずに、実作業を通してVDM専門家である技術コンサルタントからVDM++を学んだ。