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

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

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

　前回「VDMはソフトウェア開発でこう使う！ 〜導入と運用のツボ〜」では、VDM（Vienna Development Method）を開発現場に『導入』し、『運用』するためのさまざまな施策を紹介しました。

　今回からは、それらの施策を使いながら、実際どのように要求をモデリングし、仕様を記述し、仕様を検証するのかをレゴ社のLEGO Mindstorms NXT（以下、Mindstorms）を題材にして見ていきます。まず、本稿では要求を分析したうえで、VDMを前提としてモデリングをし、そのモデルをUMLで記述するところまでを紹介します。

　なお、ここからはUMLの状態遷移図やクラス図などが出てきます。これらの記法は基本的にUMLに準拠した形で記述しますが、観点としてはVDMでモデルを表現することを前提にしていますので、一般的なUML記述と比べると、多少違和感があるかもしれません。ご了承ください。

例題の要求

　今回の題材であるMindstormsはレゴブロックと制御ソフトウェアの作り方によって、さまざまな機能を持たせることが可能です（図1）。

図1　LEGO Mindstorms NXT

　今回は全体の流れを分かりやすくするため、極力シンプルな要求を用いることにします。実際に例題として用いる要求を日本語で表現すると以下のようになります。

• R1：Mindstormsは黒線の右縁に沿って走行する
• R2：電源ボタンを押下することで走行を開始し、もう一度電源ボタンを押下すると停止する
• R3：走行は、Mindstormsの左右に接続されたモーターを回転させることで前進する
• R4：Mindstormsには光センサーが備わっており、光センサーの示す値が黒であれば右ターンし、白であれば左ターンする

記述の流れ

　今回は、前回紹介した“VDMにUMLを組み合わせた記述プロセス”を取ります。具体的には、以下のような記述の手順になります。

1. 要求を読む
2. ユースケースを考え、シナリオを記述する
3. 要求とユースケースから、状態・名詞・動詞を抽出する
4. 状態遷移を定義し、状態遷移図に記述する
5. クラスと型を定義し、クラス図に記述する
6. 関数と操作を定義し、クラス図に記述する
7. 制約条件を定義し、クラス図に記述する
8. 仕様のフレームワークを検討し、仕様をブレイクダウンする

ユースケースを考える

　まずは要求をシステムにおける機能として把握するために、ユースケースを考えます。

　今回のシステムでのユースケースは「黒線の右縁に沿って走行する」です。このユースケースをもう少し詳細に記述していきましょう。

ユースケース：黒線の右縁に沿って走行する

事前条件：黒線上にMindstormsが置かれている

シナリオ：

1. 電源ボタンを押す
2. 光センサーで黒線レベル値を読み取る
3. 黒線レベル値が黒であれば右ターン、白であれば左ターンする
4. 以下、左右ターンの繰り返し
5. 電源ボタンを押す

事後条件：停止している

　要求から読み取れることをユースケース記述にすると、こんなところでしょう。

　ここで要求に対して1つ疑問がわいてきます。それは、光センサーでの黒線レベル値読み取りについてです。要求と上記のユースケース記述には、「黒線レベル値を読み取る」としか記述されていません。これでは、黒線レベル値の取り得る範囲が分かりませんし、値がどうなっていれば黒と判断するのかも分かりません。この黒線レベルに関する要求は書かれていませんので、仕様として要求に抜けている部分を定義していく必要があります。これについて、今回は以下のように取り扱うこととします。

• 光センサーで黒線レベル値を読み取る
• 黒線レベル値は「最小値」から「最大値」の範囲で値を取る
• 黒線レベル値が「黒線閾値」以下であれば黒、「白線閾値」以上であれば白とする
• 黒線閾値と白線閾値の間はグレーとし、黒／白の判断をしない

　上記では、黒線レベル値の範囲や閾（いき）値を「最小値」や「黒線閾値」としています。これらは実装ではある値を指定したり、計算したりしますが、その決め方はアーキテクチャや実験での実測値に依存します。そのため、仕様段階では具体的な値に着目せず、あえて抽象化した表現をしました。

　記述したユースケースにあるシナリオは、VDMで検証を行う際のテストケースとして使うことができますので、今回は最も簡単なシナリオのみを記述していますが、正常系・異常系を含め、複数のシナリオを用意することをお勧めします。

要求からモデルの要素を抽出する

　次に要求を分解し、モデルの要素を抽出してみましょう。前回紹介したように、VDMでのモデル抽出は要求から“状態”と“名詞”と“動詞”を抽出し、それをVDMのモデル要素として詳細化します。表1がモデルの要素として抽出した項目をカテゴリー分けしたものです。

	状態	走行中
		停止中
		黒線上
		黒線外
	名詞	Mindstorms
		黒線
		電源ボタン
		モーター
		光センサー
		黒
		白
	動詞	走行する
		停止する
		電源ボタンを押す
		右ターンする
		左ターンする
		光センサーの値を読み取る
		モーターを回転させる
表1　抽出したモデルの要素