VDMを用いた仕様記述・検証 〜 モデリング編 〜：誰でも使える形式手法（3）（3/3 ページ）

今回は「LEGO Mindstorms NXT」を題材に、要求の分析からVDMを前提としたモデリング、UMLの記述までの流れを詳しく解説する。

[植木雅幸（CSK），＠IT MONOist]

制約条件を考える

　ここでの作業は、ここまで定義した型や操作にどのような制約条件があるかを定義することです。アウトプットはクラス図にノートの形で書き込みます。これは、クラス図に制約条件を記述できないためです。もしくはクラス図にノートで書き込まず、別ドキュメントなどに記述しても構いません（注1）。

　VDMでは制約条件として、型やインスタンス変数に対する不変条件と関数や操作に対する事前・事後条件を定義できます。不変条件、事前条件、事後条件の抽出は、ここまで定義してきたインスタンス変数・型・操作に対してどのような制約条件があるかを、要求やユースケースを基に検討していきます。

　今回でいえば、制御マシンクラスに定義した操作である「右ターンする」であれば、事前条件として「黒線上にいる」、事後条件として「右ターンしている」が挙げられます。この事後条件などは一見当たり前のことですが、こういった自明な制約条件であっても、モデルが複雑になるにつれ制約条件として保証する必要が出てきますので、できるだけ自明な制約条件も定義します。また、この段階の抽象度の高いモデルですと、あまり制約条件は出ず、さらに詳細化していくにつれ制約条件が出てくることもあります。

※注1：今回はクラス図にノートとして制約条件を記述しましたが、VDMToolsでは特定のUMLモデリングツールと連携を取る機能があります。その機能を使う場合は、属性や操作の中にタグ付きの値として制約条件を記述でき、記述したクラス図からVDMのソースを生成できます。

　最後に、今回定義した制約条件を表2にまとめます。

機能名	制約条件
	事前条件	事後条件
走行する	電源ボタンがONになっている	右ターン or 左ターンしている
停止する	―	停止している
右ターンする	黒線上にいる	右ターンしている
左ターンする	黒線外にいる	左ターンしている
黒線レベルを読み取る	―	黒線レベル値が読めている
ライン状態を判定する	黒線レベル値が読めている	ライン状態の黒／白／グレーが判定できている
モーターが回転する	―	モーターが回転している
モーターが停止する	―	モーターが停止している
電源ボタンを押す	―	電源ボタンONならば電源ボタンOFF 電源ボタンOFFならば電源ボタンON
表2　制約条件一覧

　前述のような方針でクラスや型、操作をマッピングして、図3のようなクラス図を書きました。UMLのクラス図では型を定義できませんので、クラスとして定義をしたうえで型であることが分かるようにしています。

図3　クラス図

　ここまで（クラス図まで記述）できたら、次に注意すべきは、要求に対して必要な機能を満たしているか？ という点です。ユースケース記述やクラス図、状態遷移図ではレビューでしか検証できませんので、まずは目視で要求の充足を確認します。

仕様フレームワークを考える

　ここまでで、仕様の振る舞いが状態遷移図として定義され、仕様の構造がクラス図として定義されました。このままVDM記述をすることも可能ですが、現在の構造ではハードウェアであるモーターや光センサー、電源ボタンにさまざまな振る舞いがあり、責務を超えています。また、この先ハードウェアの追加や機能の追加があったときに、この構造では変更による影響がいろいろな個所に及ぶ可能性があります。

　そこで、仕様の構造と責務を少し変え、ハードウェアクラスの責務を分かりやすくシンプルにしていく必要があります。今回は、仕様のフレームワークを考えるうえでよく用いられる方法「仕様の階層化」をすることで解決していきます。具体的には、現在のモデルで制御マシンというアプリケーションと電源ボタンや光センサー、モーターといったハードウェアが直接結び付いているところに、ハードウェアを制御する中間階層を設けることにします。

　こうすることで、Mindstormsに将来さまざまな拡張による仕様追加や変更があったとしても、影響範囲を少なくできます。また、フレームワークとして枠組みを作成し、その枠組みを検証することで、この検証済みフレームワークを後々の開発まで使っていくことができるのです。

　階層化したクラス図が図4です。機能自体は変わっていませんが、ハードウェアクラスがシンプルになり、中間層であるハードウェア制御階層がモーター制御による右ターンなどを行うようになっています。

図4　階層化したクラス図

---

　今回は、VDMで記述を行う前段階として、要求をモデリングする過程を説明しました。今回モデリングをした結果、以下の3つがモデルとして定義されています。

• ユースケース
• 状態遷移図
• 階層化したクラス図

　「ユースケースは検証基準」「状態遷移図は振る舞い」「クラス図は構造」と、仕様の記述・検証に必要な要素です。VDMが難しいといわれることがありますが、難しいのは今回のように要求から仕様としてモデル化するところです。モデルができていればVDM記述は意外と単純に記述できるということを次回紹介します。お楽しみに！（次回に続く）