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

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

仕様の妥当性を検証する

　次に、仕様の妥当性確認です。プログラムに対する妥当性確認は、プログラムの「システムテスト」に当たります。つまり、“作られた最終的なプログラムが、要求どおりに作られていることを検証する”ことです。仕様検証でいうと、要求と仕様が合致しているかを確認することにほかなりません。

　この妥当性確認は、今回ユースケースで定義したシナリオをテストケースとして、要求と仕様の間の検証をしていきます。テストケースの作り方は、ユースケースのシナリオを定義する方法と同様です。VDMでは、制約条件を明確に記述できることから、シナリオの事前・事後条件を記述しやすくなっています。

　ただし、連載第3回でユースケースを定義しましたが、そのときに記述したシナリオのみでテストケースが十分であることはほとんどありません。なぜなら、連載第4回で見たように、VDMを記述していく過程でモデリング時の検討モレが出てくるからです。そこで、さらにカバレッジを見ながらシナリオを追加していく必要があります。

　妥当性確認の流れを簡単にいうと、

入力データ準備 → シナリオ実行 → 出力データ・システム状態確認

となります。

　この流れは、正当性確認と同様にVDMUnitのsetUp操作とrunTest操作を用いて簡単に記述できます。例として、レゴ社のLEGO Mindstorms NXT（以下、Mindstorms）のライントレース仕様での「右折シナリオ」を検証してみましょう。

　右折シナリオをVDMで記述すると以下のようになります。

 1 :  class testValidation01 is subclass of TestCase
 2 :    instance variables
 3 :      public iNXT : 「制御マシン」;
 4 :
 5 :    operations
 6 :      public setUp : () ==> ()
 7 :      setUp() ==
 8 :      (
 9 :        iNXT := new 「制御マシン」();
10 :        iNXT.黒線レベル値をセットする(<黒閾値以下>);
11 :      );
12 :
13 :      public runTest : () ==> ()
14 :      runTest() ==
15 :      (
16 :        iNXT.電源ボタンを押す();
17 :        iNXT.走行する();
18 :         assertTrue("test01 failed.",
19 :                    iNXT.走行状態を得る() = <走行中> and
20 :                    iNXT.進行方向を得る() = <右ターン中>);
21 :      );
22 :  end testValidation01 

　setUp操作は前述の正当性確認とほぼ変わりませんが、9行目にあるように検証する対象が「ライン監視制御」クラスからシステム全体を表す「制御マシン」になっています。runTest操作を見てみると、シナリオベースで検証しているのが分かると思います。まず、電源ボタンを入れて、その後走行させます。その結果は、Mindstormsが走行していて、setUpにてラインの状態を黒閾値以下としているため、右ターンしているはずです。これもVDMToolsを使ってテストすると図6のような画面になります。

図6　妥当性確認をVDMToolsで実行

　以上で、仕様の検証を一通り行うことができました。ここから先は、仕様変更や追加があるたびに仕様に手を入れ、回帰テストをすることで品質を保ったまま仕様を変えていきます。

　テストによって仕様の検証ができたら、次はレビューをお勧めします。なぜなら、テストでは検証できないような非機能要求、仕様の意味的整合性などは、やはり人手による検証が向いているからです。テストによる機械的検証と、人手による検証とのいいとこ取りをして、仕様の品質を高めていってください。

　以下に、ここまで記述したVDMのコードを掲載します。今回は正当性確認と妥当性確認のテストケースをそれぞれ1つずつ記述しています。この連載を読んで、「VDMに取り組んでみようかな」と考えている方、さらに関心を持たれた方は、まず今回のテストケースを参考にしていただき、そして、さらにご自身でテストケースを追加してみてはいかがでしょうか。

【 VDMのコード 】

※右クリックショートカットメニュー「対象をファイルに保存」でダウンロードしてください。

• ButtonControl.vpp
• ControlMachine.vpp
• DriveControl.vpp
• io.vpp
• LineWatchControl.vpp
• MindstormTest.vpp
• MindstormTestCase.vpp
• Motor.vpp
• OpticalSensor.vpp
• PowerButton.vpp
• VdmUnit.vpp

---

　さて、連載第3回から今回にかけて、要求を仕様としてモデル化し、VDMで仕様を記述して、さらに仕様を検証する過程を簡単に説明してきました。その流れの中で、VDMに対する具体的なイメージもつかんでいただけたかと思います。ここでぜひもう一度、連載第2回「VDMはソフトウェア開発でこう使う！ 〜導入と運用のツボ〜」を読んでみてください。連載第2回では、開発プロセスの中でVDMを導入するときに考えるべきことについて触れました。VDMに対するイメージを持ったいま、連載第2回の内容を振り返ることで、VDMを開発現場でどのように使うかが、よりはっきりと見えてくると思います。

　本連載では、形式手法の1つであるVDMを取り上げ、「実開発現場」で形式手法を「誰でも」気軽に使えるようになることを目的に解説してきました。本連載の冒頭で説明したとおり、形式手法は決して難しいものではありません。ぜひ本連載やWebサイト、書籍などを参考にして形式手法にチャレンジし、高品質仕様の下で良いシステムを作っていってください。（連載完）

◇◇ 筆者からのお知らせ ◇◇

2008年11月19〜21日の3日間、パシフィコ横浜で開催された「Embedded Technology 2008」において、筆者は「VDMとUMLを融合した仕様記述・検証の紹介」と題したワークショップを行いました。VDM公式サイトにて、その模様を動画で配信しています。ワークショップでは、VDMとUMLを融合した開発の方法とVDMToolsの新機能であるUMLリンクのデモをしています。本連載でもUMLを使ってモデルを記述していますので、興味のある方はぜひ動画も見てください。