ディペンダブル・システムのための形式手法の実践ポータル

CSK - TradeOne

ドメイン	バックオフィスシステム
開発対象	証券バックオフィスシステム TradeOne
国	日本
開発組織	CSK
形式手法（言語、ツール）	VDM++ (VDMTools)
適用範囲・規模（形式手法）	TradeOne全体のうち、マル優サブシステムとオプションサブシステムに適用した（ソースコード行数の割合では約6割）。 マル優サブシステムに関してVDM++の行数は、 ビジネスロジックが8,102行 制約が1,539行 TradeOneシステムのユーティリティが1,342行 汎用的な目的のためのユーティリティが774行 合計11,757行 オプションサブシステムに関しては、 ビジネスロジックが10,846行 テストシナリオが13,771行 テストケースが31,641行等 合計68,170行
適用対象のソフト種別	エンタプライズ系
適用目的・工程	仕様記述、設計
実装言語	C++, Java
実装規模	TradeOne全体では、1,342,858 DSI (DSIはソースコード行数とほぼ同義。COCOMOで利用される。) マル優サブシステムは18,431DSI オプションサブシステムは60,206DSI
効果	エラー発生率が、 マル優サブシステムは0件 オプションサブシステムは0.05/KDSI TradeOne非適用部分では、0.67/KDSI 生産性が、見積りよりも50-60%程度向上した。

（出典: John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat, Marcel Verhoef, Validated Designs for Object-oriented Systems, version 1.2, 2004）

詳細情報

検証内容

検証規模

テストの達成率は、C0（命令網羅）レベルで98%であった。

期間

2000-2001

判断

形式手法を利用した動機

上流工程での検証が可能であるため、高信頼性、高生産性を実現できる。

手法・ツール選択理由

障害と工夫

組織

体制

マル優サブシステム：

• 6人チーム（ひと月あたり平均4人、3.5か月間）で開発された。まずシステムアーキテクトがVDM++モデルの全体的な基本的なフレームワークを設計した。次に、4人のVDM++経験者が、並行してモデルを作成した。全てのVDM++モデルはチーム全てのメンバによってレビューされた。最後にフタルのプログラマがVDM++モデルから手動で実装した。
• 全ての開発者は40歳を越えており、ソフトウェア開発経験は20年以上あった。
• 4人は、形式手法について基本的な事前知識があった。

オプションサブシステム：

• 10人チームで開発された。
• まずドメインのエキスパートが日本語でオプションサブシステムの機能要求を記述した。
• 並行して、マル優サブシステム開発者のVDM++エキスパートの一人が、1週間以内でVDM++について指導した。
• 次に、ドメインエキスパートがオブジェクト指向のエキスパートの協力を得て、UMLでユースケースを書いた。
• 並行して、マル優サブシステム開発者であったシステムアーキテクトが、VDM++モデルの全体的なフレームワークを記述した。
• 次に、二人のVDM++エキスパートと、新しく指導された3人のプログラマがVDM++モデルを完成させた。

教育

オプションサブシステムの開発工数は合計で60.1人月であり、教育に要した時間はそのうちの2.8人月であった。

その他

情報源

• ソフトウェアコンポーネント技術に関する調査研究報告書, http://it.jeita.or.jp/eltech/report/2004/04-jou-4.html, JEITA
• John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat, Marcel Verhoef, Validated Designs for Object-oriented Systems, version 1.2, 2004, http://overtureeditor.googlecode.com/svn/trunk/Documentation/literature/VDM%20Book/bookfinal.pdf
• VDM information web site - 導入事例, http://www.vdmtools.jp/modules/tinyd1/index.php?id=5

このページの先頭へ戻る