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

状態遷移を考える

　続いて、状態遷移を考えます。ここでのアウトプットはUMLの状態遷移図です。

　VDMでは、仕様どおりに状態が遷移することだけではなく、状態が遷移したときに何をすべきか？ どのような条件があるのか？ を明らかにし、検証することを目的とします。

　先ほど抽出した状態（表1）を基に、それぞれの状態間で状態遷移が発生するトリガーやガード条件を考えて記述したのが図2の状態遷移図です。なお、この状態遷移図はMindstorms全体について記述したものであり、モーターや電源ボタンなどの個々のハードウェアに関する状態遷移については記述をしていません。

図2　状態遷移図の例

　今回の要求は非常にシンプルなものです。状態遷移もシンプルな構造になっており、電源ボタン押下による走行中と停止中、センサー値による黒線上と黒線外となっています。

仕様構造を考える

　次に、仕様の構造を考えます。仕様の構造をVDM++を前提に表現すると、オブジェクト指向の構造で表現が可能であり、UMLのクラス図に展開できます。ここでのアウトプットはUMLのクラス図です。

クラスと型を考える

　ここでの作業は、先ほど抽出した要求（表1）の「名詞」を基に、VDMにおける「クラス」と「型」を定義し、クラス図にマッピングすることです。

　クラスと型の定義にはいろいろな方法があります。システムを表す大きなクラスの中にすべての要素を型として定義してもよいですし、オブジェクト指向的にすべてをクラスで表現しても構いません。今回のモデリングでは、クラスと型のどちらに分類をするかは、その要素が振る舞いを伴うかどうか？ を基準にします。この基準に沿って、振る舞いを持つ場合はクラス、振る舞いを持たない場合は型として定義をします。

　例えば、「制御マシン（要求のMindstorms）」はシステム全体を制御する役目を持っています。その責務を考えると振る舞いとして、「走行する」や「右ターンする」が含まれてきますので、制御マシンはクラスになります。一方、「黒」や「白」は単にラインの状態を表しているにすぎず、振る舞いを持ちません。ですので、黒や白はまとめて、「ライン状態」型として定義します。

　このように仕様の構造を検討し、最終的にクラスとして定義したのは「制御マシン」「光センサー」「電源ボタン」「モーター」の4つです。それぞれのクラスに与えられた責務は以下のとおりです。

• 制御マシン：システム全体の制御を責務とする。システムの状態に応じて、各ハードウェアに対して命令をする
• 光センサー：黒線レベル値を読み取り、黒線レベルを判定する
• 電源ボタン：電源ボタンが押されているか否かの状態を制御する
• モーター：モーターの回転と停止を制御し、Mindstormsの前進と停止を担う

状態をクラスの属性と対応付ける

　ここでの作業は、先ほど抽出した要求（表1）の「状態」をどのクラスが管理するのかを決定し、それをクラス図に属性としてマッピングすることです。

　状態はモデルの中でも常に変化していく性質を持っています。VDMでは、一般的に状態をインスタンス変数として取り扱います。

　例えば、「走行中」「停止中」「黒線上」「黒線外」のような状態は、システム全体の状態を表しているといえますので、制御マシンクラスが管理すべき状態です。そこで、これらの状態をまとめて「走行状態」として定義をしています。また、電源ボタンON／OFFやモーターの回転／停止、光センサー黒／白などは各ハードウェアが管理すべき状態ですので、各クラスの属性として定義をします。

関数・操作を考える

　ここでの作業は、先ほど抽出した要求（表1）の「動詞」を基に、VDMにおける「関数」と「操作」を定義し、クラス図にマッピングすることです。関数と操作の定義は、VDMでは明確に分ける必要がありますが、UMLでは明確に分けることができませんので、クラス図では「操作」としてすべて扱います。

　操作の定義は、まず抽出した動詞を機能ととらえ、その機能をどのクラスが責務として担うかのマッピングをすることです。そして、その操作の入出力を定義するところまででひとまず完成です。

　例えば、動詞で抽出した「走行する」や「右ターンする」はシステム全体の制御になりますので、制御マシンクラスが責務を担います。一方、「光センサーの値を読み取る」や「モーターを回転させる」は、光センサークラスやモータークラスといった個別のクラスで責務を担うような振る舞いですので、各クラスに振る舞いをマッピングします。

　また、入出力に関しては、モータークラスに定義した「回転する」操作の場合、何らかの回転速度を入力として、モーターを回転させると定義しました。ただ、この段階では回転速度をどのように入力として与えるかはアーキテクチャや設計に依存する部分であるため、VDMの組み込み型である「token型（型を確定せず、後で決定したいような場合に使う型）」で定義をしました。光センサークラスに定義した「黒線レベルを読み取る」操作では、読み取った黒線レベルの値を返す必要があると定義をしています。