TradeOne

グでは、学習者の教育的背景(大学での専攻など)は形式手法の習得には大きな障害にはな らならず、むしろドメイン知識を持っていることは習得に非常に役立った、というコメン トを得た。

(2) 実作業による習熟

SPARKを習得した技術者は全員Z記法を読むための教育も受けた。SPARKによる設計お

よび実装についてはクラスルーム形式の教育を受講後、直ちに実務に着いて作業を遂行す ることができた。

SPARK を扱う作業としては、実行時例外に関する証明があった。この作業にあたるため

には、2ヶ月の習熟期間を要した。

(3) Z記法／SPARK以外の記法やツールに関する教育

Z 記法および SPARK 以外には、このプロジェクトではユーザインタフェースに関する仕 様記述として状態表が用いられた。状態表については特に教育は必要なく、直ちに理解さ れた。

また、テスト用の参照実装のために Mathematica が使われたが、5 人のみがトレーニング を受けた。

(4) 教育コストの影響

開発側企業は、教育コストは大きな問題ではなかったとしている。多種多様な背景を持つ スタッフに対して教育が行われたが、大きな困難はなかったとしている。例えば Z 記法の コースは 3 日間であり、一度受講すればそれで十分であり、コストとしても安上がりだっ たとしている。

設計言語 UML, 設計用共通フレームーク利用, 日本語 実装言語 C++

開発 日 SCSK株式会社（旧 日本フィッツ株式会社）

ドメイン 証券業務

4.6.2 プロジェクト概要

証券会社のバックオフィス機能を提供する TradeOne パッケージの開発に際し、一部サブ システムの開発に形式仕様記述言語VDM++が採用された。

開発対象となったのは

• マル優

• オプション取引

の 2 つのサブシステムである。パッケージ全体の開発としては、普通のオブジェクト指向 開発手法（UML+繰り返し開発）が採用されていたが、上記のサブシステム開発を引き受 けたメンバーの発案により形式仕様記述の採用が決定された。

基本的に外販用パッケージを開発する目的でプロジェクトが進んでいたため大部分の要求 は社内の証券ドメイン専門家を交えた商品企画部門から出されていたが、最初の顧客（証 券会社）のためのカスタマイズ要求も一部含まれていた。

当時、証券業務の複雑な処理は永年の経験によって暗黙的に蓄積され、設計、実装、検証 されていたが、形式仕様記述を利用することによって、業務ルールが明示的に記述され、

それまで証券業務を知らなかった設計実装者も、急速に問題領域の知識を得て、仕様の矛 盾を指摘できるようになった。

4.6.3 開発プロセス概要

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

マル優の開発とオプション取引の開発は異なる所もあるが、全体として似通った部分の方 が多いため、以下1つのプロジェクトとして説明を行うことにする。

図4-11: 開発プロセスの全体像[HS06]

原始要求は大部分社内の商品企画からきているが、一部最初のパッケージ顧客からのカス タマイズ要求も取り込まれたものになっていた。こうした要求は要求分析チームによって 主にユースケース記述としてまとめられたが、まだ厳密さには欠けていたので、仕様策定 チームがユースケースに対応するシナリオを起点に VDM++を用いた仕様策定を行い、仕 様アニメーションの形で検証を行った。

記述された機能仕様をもとに、設計実装チームが C++を用いたシステムとして実装を行っ た。すなわち仕様を見ながら設計実装チームが手で設計実装を行ったわけであるが、この 作業に際して、単純な仕様から設計への展開ガイドラインを作成する代わりに、仕様から 設計実装への橋渡しを行いやすくするフレームワーク Gofo を準備して、実際の開発作業 に適用した。

要求分析チームは証券業務の知識はあるが、形式仕様の経験はない。仕様策定チームは一 部古い証券業務の知識はあるものの特に問題領域知識に対する強みはない形式仕様記述の 専門家であり、設計実装チームは様々な実現手段を持っていたものの、証券業務の知識も 形式手法の経験もなかった。FW 検討コンサルタントは形式手法の知識と事務処理業務の 知識を持っていたが、証券業務の知識は持っていなかった。

表4-11: チームとその特性

チーム名 特性

要求分析チーム 証券業務の知識を持つ専門家。形式仕様の経験はなし。

抽象化を通したモデリングの経験もほとんど持っていな かった。

仕様策定チーム 形式仕様記述の専門家。

一部のメンバーは形式仕様記述に関して深い知識は持つ ものの証券業務知識は皆無であり、また一部のメンバーは 古い証券業務知識をもっていたが、形式仕様記述に関し

ては当初深いレベルには達していなかった。

設計実装チーム 設計／実装の専門家。実装言語を問わず様々な実現手段 を身につけていた。

形式仕様記述の経験も証券問題領域の専門知識も持ち 合わせていなかった

FW検討コンサルタン ト

設計実装のためのアーキテクチャを検討し、形式仕様から 設計実装の流れの中で利用しやすいように、アーキテク チャをフレームワークの形に落とし込んだものを提供した。

ある程度の形式仕様記述の知識と、幾つかの事務処理問 題領域に関する知識は持ち合わせていたが、証券業務そ のものの知識は持ち合わせていなかった

4.6.4 記述と支援ツール

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

表4-12: 使用された記述と主なツール

記述 ツール 適用内容

VDM++ VDMTools 構文検査、型検査、仕様アニメーション

Gofo フレームワーク 設計実装のためのフレームワーク。当時はまだ

珍しかったウェブアプリケーション開発のため のフルスタックのフレームワークをまず設計し、

それとVDM++仕様との対応関係を示すことに

より仕様から設計への円滑な橋渡しを可能にし た。

Gofoは事務処理に特化した問題領域の知識 を表現する語彙（伝票、帳簿、業務論理、事務 員など）を用いるため、仕様と設計の対応関係 をとりやすい構造になっている。

4.6.5 厳密な仕様記述の効果

(1) 仕様の早期検証による妥当性確認 (validation) の効率化

仕様アニメーションを通して早い段階でシナリオを通した仕様の検討ができたため、要求 を出す側との意見調整と仕様に対する意思決定を素早く行う事ができた。

(2) 設計への円滑な橋渡し

既に説明したように、設計実装フレームワーク（Gofo）が用意され、仕様との対応関係を 明確にするようにしてあった。VDM++による仕様に書かれた内容が、設計のどの部分に反 映されるべきかが決まっていたため、仕様を設計に反映する作業も円滑に進み実装上のつ まらないミスも発生しにくい形になっていた。

(3) 業務知識（問題領域知識）の移転

表 4-11：チームとその特性 からもわかるように説明したように、開発が始まった段階で

は要求分析チームのメンバー以外は証券業務に関しては深い知識を有していなかった。

しかし開発が進むにつれて、少なくとも開発対象業務の性質については深く理解できるよ うになっていった。これは要求に現れる業務を抽象化して厳密な記述として、皆が読める ような形になったことによるものであった。

その意味で形式仕様記述は、業務知識の効果的な移転ツールの役割も果たしたと言う事が できる。

(4) 高品質なシステムの実現

仕様アニメーションを用いた早期からの検証により、仕様レベルでの品質はとても高いも のになった（設計、実装レベルの品質はフレームワークに作り込まれた）。仕様策定段階 でも、繰り返し仕様アニメーションによる回帰テストが実施され、仕様の間違いが探され 続けた。

このため最初の本番システムリリース後、本サブシステムに関しては本質的不具合が 1 件 も報告されなかった（1 件だけマイナーな不具合が帳票レイアウト上に発見されたが、そ の部分は形式仕様記述の範囲外であった）。

(5) 低保守コストの実現

TradeOne には複数のサブシステムが存在していたため、他のサブシステムとの生産性が

比べられた。この計算を最初に行ったときには、形式手法を用いた当サブシステムと、通 常の開発手法を採用した他の 2 つのサブシステムの間では「リリースまでの生産性」は似 通っていた。

このため形式手法はあまり効果がなかったのかという意見も出されたが、結局リリース後 形式手法を用いたサブシステムでは 1 件も不具合が発生しないのに比べて他のサブシステ ムでは複数の不具合が発生し、パッケージ改修費用などがコストとして発生していた。

この意味で保守までを含んで考えた場合、本プロジェクトに関しては形式手法を用いたほ うが保守コストを低くできることがわかった。

なお最初の開発における生産性には、それまで存在していなかった様々な準備（仕様記述 の形式、フレームワークの検討と作成、仕様検証の為の枠組みの作成、仕様ライブラリの 整備）などが含まれている。上記理由から更に生産性が高くなると予想される。