株式会社ジェーエフピー

VDM

VDM

電気ポットの「企画要求仕様」(リスト1)を題材にします。以下の5項目の要求が書かれています。

リスト1 企画要求仕様

PR01: 電気ポットの容量は2リットルとし、10度Cから沸騰するまでの時間は、15分以内とする。
PR02: 電源コンセントをつなぐと、直ちに作動し、ヒータで加熱を始め、沸騰に達したら、90度Cに保温する。
PR03: 再沸騰ボタンが押されたら、再沸騰を始める。
PR04: 水が加えられ、温度が低下したら、再沸騰を始める。
PR05: 保温中であれば、お湯を注ぐことができる。

分析者は、まず、企画要求の一覧(図1)を作り、要求を機能要件と非機能要件に分類しました。

図1 企画要求の一覧

続いて、分析者は、要求から状態、クラス、型、操作を抽出する作業を行いました。この作業を「要求分析」(図2)と称します。

図2 要求分析

続いて、分析者はデータフロー図(図3)を作成しました。ここまでの作業はMicrosoft Excelを使用しました。

図3 データフロー図

最後に、VDM++形式(リスト2)で仕様を記述しました。ツールはOvertureを使用しました。

リスト2 VDM++

------------------------------------------
class 「システム」
instance variables public i水温監視 : 「水温監視」; public i水温制御 : 「水温制御」; public i給湯制御 : 「給湯制御」; operations public 「システム」 : () ==> 「システム」 --初期化 「システム」() == ( i水温監視 := new 「水温監視」(); i水温制御 := new 「水温制御」(i水温監視); i給湯制御 := new 「給湯制御」(i水温制御); start(i水温監視); start(i水温制御); ); public 再沸騰させる : () ==> () 再沸騰させる() == i水温制御.再沸騰させる(); public お湯を注ぐ : () ==> () お湯を注ぐ() == i給湯制御.給湯する(); end 「システム」
-------------------------------------------
-------------------------------------------
class 「水温監視」
types
public 「水温」 = <低温> | <高温> | <沸点> | <異状>; --高温=90℃「前後」 instance variables
public i水温 : 「水温」 := <低温>; operations
protected 水温を監視する : () ==> () 水温を監視する() == is not yet specified post i水温 = 水温センサの値を得る(); pure protected 水温センサの値を得る : () ==> 「水温」 水温センサの値を得る() == is not yet specified; thread
while true do 水温を監視する(); end 「水温監視」
-------------------------------------------
-------------------------------------------
class 「水温制御」
types
public 「動作モード」 = <停止中> | <沸騰中> | <保温中>; instance variables
public i動作モード : 「動作モード」; protected i水温監視 : 「水温監視」; operations
public 「水温制御」 : 「水温監視」 ==> 「水温制御」 「水温制御」(a水温監視) == ( i水温監視 := a水温監視; ); public 再沸騰させる : () ==> () 再沸騰させる() == is not yet specified post i動作モード = <沸騰中>; pure protected 動作モードを決定する : () ==> 「動作モード」 動作モードを決定する() == is not yet specified post cases mk_(i水温監視.i水温, RESULT): mk_(<沸点>,<保温中>) -> true, mk_(<沸点>,<沸騰中>) -> false, mk_(<高温>,<保温中>) -> true, mk_(<高温>,<沸騰中>) -> true, mk_(<低温>,<保温中>) -> false, mk_(<低温>,<沸騰中>) -> true, mk_(<異状>,<停止中>) -> true, others -> false end and i動作モード = RESULT; protected ヒータを制御する : () ==> () ヒータを制御する() == is not yet specified post i動作モード = 動作モードを決定する(); thread
while true do ヒータを制御する(); end 「水温制御」
-------------------------------------------
-------------------------------------------
class 「給湯制御」
instance variables
protected i水温制御 : 「水温制御」; operations
public 「給湯制御」 : 「水温制御」 ==> 「給湯制御」 「給湯制御」(a水温制御) == ( i水温制御 := a水温制御; ); public 給湯する : () ==> () 給湯する() == is not yet specified pre i水温制御.i動作モード = <保温中>; end 「給湯制御」
-------------------------------------------

参考までに、別の分析者がVDM-SLで記述したものをリスト3に示します。このVDM-SLの記述はOvertureにインポートして見ることができます。

リスト3 VDM-SL

/* * PR01 : 電気ポットの容量は 2 リットルとし、10 度 C から沸騰するまでの時間は、15 分以内とする。
*
* PR02 : 電源コンセントをつなぐと、直ちに作動し、ヒータで加熱を始め、沸騰に達したら、90 度 C に保温する。
*
* PR03 : 再沸騰ボタンが押されたら、再沸騰を始める。
*
* PR04 : 水が加えられ、温度が低下したら、再沸騰を始める。
*
* PR05 : 保温中であれば、お湯を注ぐことができる。
*/

types
水量型 = int /* 単位はミリリットルとする。 */
inv 水量 == 0 <= 水量 and 水量 <= 2000; /* PR01 */
水温型 = int /* 単位は摂氏とする。 */
inv 水温 == 0 <= 水温 and 水温 <= 100;
ポットの状態型 = <電力が供給されていない> | <沸騰するまで加熱せよ> | <保温せよ>;
ヒーターの状態型 = <停止> | <加熱> | <自動>
/* 「自動」とは、保温のために自動的にONとOFFを切り替えることである。 */

values

state ポット of
ポットの状態: ポットの状態型 ヒーターの状態: ヒーターの状態型 水量: 水量型 水温: 水温型 init
状態 == 状態.ポットの状態 = <電力が供給されていない> and 状態.ヒーターの状態 = <停止>> and 0 < 状態.水量 and 状態.水量 <= 2000 and 0 <= 状態.水温 and 状態.水温 < 100 inv
状態 == true end