VDMを用いた仕様記述・検証 ～ モデリング編 ～

今回は「LEGO Mindstorms NXT」を題材に、要求の分析からVDMを前提としたモデリング、UMLの記述までの流れを詳しく解説する。 前回「VDMはソフトウェア開発でこう使う！ ～導入と運用のツボ～」では、VDM（Vienna Development Method）を開発現場に『導入』し、『運用』するためのさまざまな施策を紹介しました。 今回からは、それらの施策を使いながら、実際どのように要求をモデリングし、仕様を記述し、仕様を検証するのかをレゴ社のLEGO Mindstorms NXT（以下、Mindstorms）を題材にして見ていきます。まず、本稿では要求を分析したうえで、VDMを前提としてモデリングをし、そのモデルをUMLで記述するところまでを紹介します。 なお、ここからはUMLの状態遷移図やクラス図などが出てきます。これらの記法は基本的にUMLに準拠した形で記述しますが、