|
[2007 年 2 月号] |
［技術講座］
私は主に組み込み分野における開発に携わってきました。近年、組み込み分野では、品質に対する要求はどんどん厳しくなっています。現在、品質向上のための様々なアプローチが行われています。今回は、人間にわかりやすいモデルを、抜け漏れなく検証するという観点で、UMLとモデル検証の組み合わせの可能性を探ってみました。
本記事では、UMLの状態マシン図で記載したモデルに、モデル検証ツールspinを適用していきます。
spinとは、ベル研究所で開発されたオープンソースのモデル検証ツールです。検証対象のモデルの取りうる全ての状態において、検証条件を満たしているか確認することができます。また、複数のタスクで動作するシステムにおけるデッドロックの発生なども検出することができます。デッドロックの検出例は、書籍やWebサイトでも多く紹介されています。
組み込みシステムにおいては、現在でもRTOS（リアルタイムOS）無しで、周期動作するメインループ中心の動作メカニズムが採用されるケースが多くありますが、このようなケースでもspinを用いてモデル検証を行うことができます。本記事ではこういったケースでどのようにモデル検証を行うのか紹介します。
今回は分析対象として、タイマ機能付きのテレビを取り上げます。このテレビはリモコンなどによる電源のON/OFF以外に、ONタイマとOFFタイマによる電源ON/OFFを行うことができます。
ONタイマ
- 時刻（HH:MM）でセットする。1分単位でセット可能。
- ONタイマ設定時刻になった時に、電源OFFなら電源ONにする。このときONタイマ設定は解除される。
- ONタイマキャンセル操作を行うと、ONタイマ設定は解除される。
OFFタイマ
- 時間（n分後）でセットする。1〜120分後まで1分単位でセット可能。
- OFFタイマ設定時間が経過した時に、電源ONなら電源OFFにする。
- 電源がOFFになったら、OFFタイマ設定は解除される。
- OFFタイマキャンセル操作を行うと、OFFタイマ設定は解除される。
では、分析対象をUMLでモデリングしてみます。対象が電源ON/OFFといった状態を持ち、時間の経過に伴う動作が、その状態によって異なることなどから、ステートマシン図を用いてモデリングすることにします。
＜図3.1.タイマ付きテレビ＞基本的な状態遷移は、図3.1に示すとおりです。今回は、ONタイマやOFFタイマを実現するためにシステムが提供するタイマを利用することを想定しています。システムが提供するタイマは、セットとクリアが可能で、セットしてからクリアされるまでの間カウントを継続します。また、セットした時間を経過するとタイムアウト状態になります。これを踏まえて、図3.1のモデルにタイマのセットとクリアを盛り込んだモデルが、図3.2です。
＜図3.2.タイマ付きテレビ（タイマ操作記載）＞
4.1.ツールの準備
さて、いよいよ作成したUMLモデルを検証するわけですが、その前にいくつか準備が必要です。
まず、モデル検証ツールのspinのインストールです。spinは、https://spinroot.com/spin/Man/README.htmlから、ダウンロードすることができます。さらに、spinで作成する検証用のC言語のプログラムをコンパイルするために、Cコンパイラを用意しておきましょう。
spinでモデルの検証を行うためには、検証対象のモデルを検証用の言語promelaで記述する必要があります。promelaはC言語に似た文法を持つ言語です。言語仕様の詳細は、https://www.spinroot.com/spin/Man/promela.htmlに記載されています。
4.2.モデルの動作方式決定
spin上でモデル検証を行うためには、モデルをどのように動作させて検証するかという方針を決める必要があります。このとき、最終的な設計・実装イメージと同じ方式で検証すれば、検証されたモデルと同じ方式で実装することになるため、効果的です。
＜図4.1.検証モデルの動作方式＞今回は、モデルを周期的に動作させる方式をとることにします。シングルタスクあるいは、RTOS無しの環境で、モデルが周囲の状況に応じて動作するイメージです。よって、図4.1に示すように検証モデルが動作し、その結果を検証し（詳細は後述）、タイマなどのアーキテクチャメカニズムを動作させ、最後に電源ON/OFFやタイマ設定/キャンセルなどの要求を取得します。この流れを繰り返すわけです。
※新たに登場したpromela言語要素： active, proctype, do-od
ソースコード4.1.検証モデルの骨格部active proctype main() { do :: /* 検証モデル動作 */ /* 検証 */ /* アーキテクチャメカニズム動作 */ /* 要求シミュレーション */ od }では、この一連の流れをpromelaで記載してみましょう。まず、active proctype main()と記述します。activeは、自動起動することを意味し、proctypeはプロシージャの宣言を意味します。mainはプロシージャの名前です。mainプロシージャの中にはdoループが存在し、これはdo-odで囲まれた部分を::以後に示す条件を満たす限り繰り返すことを意味します。::の後に何も書かなければ、無条件のループとなります。現段階では、ループの中身は単なるコメントとなっています（promelaではC言語スタイルのコメントが使用できます）。ここから、それぞれのコメントに対応する処理を呼び出していく方針です。
※新たに登場したpromela言語要素： inline
ソースコード4.2.要求シミュレーションの呼び出しソースコード4.2に示すように、要求を擬似的に発生させる処理をinlineとして定義します。inlineは、C言語の関数型マクロのように、呼び出し元の位置に、呼び出し先の内容が挿入される形で動作します。inlineの呼び出しよりも前に、定義をしておく必要があります。
4.3.要求のシミュレーション部作成
要求には、電源のON/OFF要求、ONタイマ設定/キャンセル要求、OFFタイマ設定/キャンセル要求があります。まず、これらの要求を呼び出す部分をソースコード4.3に示します。中身は、下請けのinline定義を呼び出しているだけです。
ソースコード4.3.要求のシミュレーションinline req_sim() { req_sim_power(); /* 電源要求 */ req_sim_on_tim(); /* ONタイマ要求 */ req_sim_off_tim() /* OFFタイマ要求 */ }まず、電源ON/OFF要求から見ていきましょう（ソースコード4.4）。
※新たに登場したpromela言語要素： mtype, chan, empty, nempty, ?, _, break, if-fi, !, skip
ソースコード4.4.電源ON/OFF要求mtype = { REQ_NONE, REQ_OFF, REQ_ON, REQ_CAN, REQ_SET } chan req_power = [1] of { mtype } inline req_sim_power() { do :: empty(req_power) -> break :: nempty(req_power) -> req_power?_ od; if :: req_power!REQ_OFF :: req_power!REQ_ON :: skip fi }最初にmtypeの定義を行っています。mtypeを用いることで、任意のラベルをユニークな値として定義できます。C言語のenumのようなイメージです。しかし、全てのmtype定義を通して、ラベルの値がユニークである点がC言語のenumとは異なります。また、promelaではCの標準ライブラリのprintfに似た、その名もprintf関数がサポートされていますが、printf("%m", LabelName)という呼び出しを行うと、ラベルが文字列で出力されます。
次に、req_powerをmtypeを通信内容とする、長さ1のチャネルとして宣言および初期化しています。チャネルは、プロセス間でデータを送受信するためによく利用されます。今回、プロセスは一つですが、擬似的な要求の発行と取得の目的で利用しています。
inline定義req_sim_powerの中身は、大きく2つに別れています。ひとつは、チャネルの中身のクリア。もうひとつは、ランダムな要求決定および要求の送信です。
チャネルの中身のクリアでは、（後ほど実装する）検証対象によって要求が消費されてもされなくても、チャネルを空の状態に戻しています。promelaのチャネルは、長さ分のメッセージが入っているとき（一杯のとき）さらに送信しようとすると、チャネルに空きができるまで送信側がブロックしてしまいます。これを防ぐために、中身をクリアしているわけです。中身をクリアするには、チャネルが空になるまで受信を行う必要があります。受信は、"チャネル名?受信結果格納変数"という構文で行います。今回は、受信結果格納変数に『_』を指定することで中身を捨てています。nullデバイスのようなイメージです。
ここで『->』というseparatorを用いていますが、これは『;』と全く同じ意味で、単なる文の区切りです。慣習的に、条件式の後に利用されます。『;』の使い方も含め、詳細は、https://www.spinroot.com/spin/Man/separators.htmlを参照して下さい。『;』の使い方はC言語と若干異なります。ただし、実際のspin実装では、文法チェックを甘く設定しているため、C言語っぽく書いても、（将来に渡って動作する保証はありませんが）多くの場合問題なく動作します。
ランダムな要求の決定は、if-fi文で行います。promelaのif-fi文やdo-odループでは、::の後にガード条件を記載し、ガード条件が成立した場合にのみ以後の処理を行います。複数のガード条件が成立した場合は、そのうちのいずれかがランダムに選択されます。また、ガード条件に何も記載しなかった場合は、条件成立と見なされます。ソースコード4.4では、ガード条件が記載されていないため、全て無条件に成立と見なされ、『REQ_OFFの送信』、『REQ_ONの送信』、『何も送信しない』の、いずれかの処理がランダムに選択されます。
同様に、ONタイマ、OFFタイマに関する要求も記述します。ここでは、OFFタイマに関する要求のみ紹介します（ソースコード4.5）。
※新たに登場したpromela言語要素： #define, byte, ++
ソースコード4.5.OFFタイマ要求#define OFF_TIM_MAX 120 /* 120分まで設定可能 */ chan req_off_tim = [1] of { mtype, byte } inline req_sim_off_tim() { byte off_set = 1; do :: empty(req_off_tim) -> break :: nempty(req_off_tim) -> req_off_tim?_, _ od; if :: req_off_tim!REQ_CAN, 0 :: do :: off_set < OFF_TIM_MAX -> off_set++ :: off_set >= OFF_TIM_MAX -> break :: break od; req_off_tim!REQ_SET, off_set :: skip fi }電源ON/OFF要求と異なる点は、チャネルで複数のメッセージ（要求種別と設定時間）を送信している点と、設定時間をdo-odループを用いてランダムに設定している点です。
4.4.アーキテクチャメカニズムの作成
要求のシミュレーション部ができたので、次に、アーキテクチャメカニズムを動作させる部分を作っていきます。といっても今回は、ONタイマとOFFタイマをセットしたり進めたりする機能だけです。ソースコード4.6に示すように、mainプロシージャのdo-odループから、inline定義されたarch_mecを呼び出し、その中で、それぞれのタイマを進めています。
ソースコード4.6.アーキテクチャメカニズムの動作ここでは、OFFタイマに関連する動作を取り上げて説明します。まず、OFFタイマのクラス図を図4.2に示します。
＜図4.2.OFFタイマ＞これに対応するpromelaソースコードが、ソースコード4.7になります。
※新たに登場したpromela言語要素： bool, false, true
ソースコード4.7.OFFタイマ関連操作/* OFFタイマ */ /* 有効フラグ */ bool enable_off_tim = false; /* 設定時間 */ byte set_off_tim_val; /* 経過時間 */ byte cur_off_tim_val = 0; /* 発火通知 */ chan is_fire_off_tim = [1] of { bool } inline set_off_tim(val) { cur_off_tim_val = 0; set_off_tim_val = val; enable_off_tim = true } inline clr_off_tim() { enable_off_tim = false } inline tick_off_tim() { if :: enable_off_tim == true -> cur_off_tim_val++; if :: cur_off_tim_val == set_off_tim_val -> if :: empty(is_fire_off_tim) -> is_fire_off_tim!true :: nempty(is_fire_off_tim) -> skip fi :: else -> skip fi :: else -> skip fi }クラス図の属性と操作を、promelaの言語要素に対応付けながら実装します。設定時間、現在時間、有効無効情報という3つの属性は、それぞれset_off_tim_val、cur_off_tim_val、enable_off_timという変数に対応付けました。セット、クリア、進めるという操作は、それぞれ、set_off_tim、clr_off_tim、tick_off_timというinline定義に対応付けました。時間経過確認という操作は、チャネルis_fire_off_timに対応付けました。
tick_off_timにおいて、:: else -> skipと記述している箇所が2カ所あります。:: else -> skipは、『それ以外なら何もせずに進む』という意味です。promelaは、ガード条件が成立しない場合、成立するまでそこでブロックします。もし、最初の:: else -> skipが無ければ、cur_off_tim_val == set_off_tim_valが成り立つまでその場でブロックしてしまいます。他のプロセスが、これらの変数を書き換えて、いずれ条件が成立するのを待つようなケースならよいですが、今回はそのような想定ではありません。そもそも今回は、シングルプロセスのモデルです。そんなわけで、このような記述をしています。
ONタイマに関しても同様に定義しますが、ここでは省略します。
さて、ここまでで検証対象のモデルを動作させる仕組みが完成しました。いよいよ、検証対象のモデルをpromelaで実装していきます。
5.1.状態の実装
まず、ソースコード5.1に示すように、UMLモデルに対応する状態をmtypeで宣言します。現在の状態は、2つの変数で実装しました。2つの変数とは、コンポジット状態を表す変数をsと、サブ状態を表す変数をssで、それぞれUMLモデルに従って初期化しています。次に、検証対象のモデルをinline定義tvとして実装します。
ソースコード5.1.状態モデルmtype = { S_OFF, S_ON } mtype = { S_OFF_T_NONE, S_OFF_T_ON } mtype = { S_ON_T_NONE, S_ON_T_OFF, S_ON_T_ON, S_ON_T_OFF_ON } /* 状態 */ mtype s = S_OFF; mtype ss = S_OFF_T_NONE; inline tv() { if /* 電源OFF中 */ :: (s == S_OFF) -> if /* タイマセット無し */ :: (ss == S_OFF_T_NONE) -> skip /* ONタイマセット中 */ :: (ss == S_OFF_T_ON) -> skip :: else -> skip fi /* 電源ON中 */ :: (s == S_ON) -> if /* タイマセット無し */ :: (ss == S_ON_T_NONE) -> skip /* OFFタイマセット中 */ :: (ss == S_ON_T_OFF) -> skip /* ONタイマセット中 */ :: (ss == S_ON_T_ON) -> skip /* ONタイマOFFタイマセット中 */ :: (ss == S_ON_T_OFF_ON) ->skip :: else -> skip fi :: else -> skip fi } active proctype main() { do :: /* 検証モデル動作 */ tv(); /* 検証 */ /* アーキテクチャメカニズム動作 */ arch_mec(); /* 要求シミュレーション */ req_sim() od }まずは、状態に対応するif-fi文を記述します。この段階では、全ての条件成立時の処理を、暫定的にskipにしておきます。
状態ラベルとUMLモデルの状態は、図5.1に示すように1対1に対応しています。
＜図5.1.状態ラベルとUMLモデルの関係＞5.2.遷移の実装
状態の実装までできたので、次に、遷移の実装を行います。先ほど、暫定的にskipにしておいた部分に、それぞれ遷移を記述します。まずは、『電源OFF中-タイマセット無し』状態からの状態遷移を、ソースコード5.2に示します。
※新たに登場したpromela言語要素： ?[]
ソースコード5.2.『電源OFF中-タイマセット無し』状態からの状態遷移/* タイマセット無し */ :: (ss == S_OFF_T_NONE) -> if :: req_power?[REQ_ON] -> req_power?_; printf("POWER ON\n"); s = S_ON; ss = S_ON_T_NONE :: else -> skip fiUMLモデルに従って、電源ON要求があれば『電源ON中-タイマセット無し』状態へ遷移し、そうでなければskipしています。skipは、何もしないという意味なので、現状態に留まります。チャネルからの受信時、?の右に受信バッファの代わりに定数を設定すると、その定数とチャネルの内容が一致した時のみ条件が成立します。さらに?の右を[]で囲んでいます。これは、チャネルの中身を消費せずに確認することを意味します。いわゆるポーリングです。ここでポーリングせずに、[]無しの通常受信を行うと、その下の::elseの使用がエラーとなります。詳細は、https://www.spinroot.com/spin/Man/else.htmlを参照して下さい。なお、条件成立後は、req_power?_;のように通常受信してチャネル内容を消費しています。
同様に全ての遷移を実装していきます。全ては紹介しきれないので、ソースコード5.3に示す、『電源ON中-OFFタイマセット中』状態からの状態遷移について簡単に説明します。
ソースコード5.3.『電源ON中-OFFタイマセット中』状態からの状態遷移/* OFFタイマセット中 */ :: (ss == S_ON_T_OFF) -> if :: is_fire_off_tim?[true] -> is_fire_off_tim?_; clr_off_tim(); printf("OFF TIMER FIRED\n"); s = S_OFF; ss = S_OFF_T_NONE :: req_power?[REQ_OFF] -> req_power?_; clr_off_tim(); printf("POWER OFF\n"); s = S_OFF; ss = S_OFF_T_NONE :: req_on_tim?[REQ_SET] -> req_on_tim?_, req_on_tim_val_h, req_on_tim_val_m; set_on_tim(req_on_tim_val_h, req_on_tim_val_m); printf("ON TIMER SET[%d:%d]\n", req_on_tim_val_h, req_on_tim_val_m); ss = S_ON_T_OFF_ON :: req_off_tim?[REQ_CAN] -> req_off_tim?_, _; clr_off_tim(); ss = S_ON_T_NONE :: else -> skip fiUMLモデルにおける遷移と、promelaのif文の対応を、図5.2に示します。このように、遷移を機械的にif文のガード条件にマップしていき、条件が成立したとき状態変数を遷移先状態に更新すればよいわけです。
＜図5.2.promelaのif文とUMLモデルの遷移の関係＞
ここまでで、UMLモデルをpromelaで実装することができました。いよいよ、モデル検証の内容を作っていきます。検証の内容は様々に考えることができますが、今回は、メインの機能であるONタイマとOFFタイマの設定の正しさについて検証してみます。
まず、どの状態でONタイマが有効なのか考えてみると、『電源OFF中-ONタイマセット中』、『電源ON中-ONタイマセット中』、『電源ON中-ONタイマOFFタイマセット中』の3状態であることが分かります。逆に、これ以外の状態では、ONタイマが無効であるべきといえます。OFFタイマについても同様に考えます。その結果を、ソースコード6.1に実装します。検証したい式は、assert(成り立つべき条件)という形式で記述します。
※新たに登場したpromela言語要素： assert
ソースコード6.1.モデル検証の内容inline check_model() { printf("STAT [%e\t:%e\t]\n", s, ss); if /* 電源OFF中 */ :: s == S_OFF -> if /* タイマセット無し */ :: ss == S_OFF_T_NONE -> assert(enable_on_tim == false); assert(enable_off_tim == false) /* ONタイマセット中 */ :: ss == S_OFF_T_ON -> assert(enable_on_tim == true); assert(enable_off_tim == false) :: else -> skip fi /* 電源ON中 */ :: s == S_ON -> if /* タイマセット無し */ :: ss == S_ON_T_NONE -> assert(enable_on_tim == false); assert(enable_off_tim == false) /* OFFタイマセット中 */ :: ss == S_ON_T_OFF -> assert(enable_on_tim == false); assert(enable_off_tim == true) /* ONタイマセット中 */ :: ss == S_ON_T_ON -> assert(enable_on_tim == true); assert(enable_off_tim == false) /* ONタイマOFFタイマセット中 */ :: ss == S_ON_T_OFF_ON -> assert(enable_on_tim == true); assert(enable_off_tim == true) :: else -> skip fi :: else -> skip fi; /* タイマのカウント値 */ assert(cur_on_h <= ON_TIM_H_MAX); assert(cur_on_m <= ON_TIM_M_MAX); assert(cur_off_tim_val <= OFF_TIM_MAX) } active proctype main() { do :: /* 検証モデル動作 */ tv(); /* 検証 */ check_model(); /* アーキテクチャメカニズム動作 */ arch_mec(); /* 要求シミュレーション */ req_sim() od }次に、タイマのカウント値について考えてみます。これは、状態にかかわらず上限を超えないはずです。なお、タイマ上限は
#define OFF_TIM_MAX 120 #define ON_TIM_H_MAX 24 - 1 #define ON_TIM_M_MAX 60 - 1このように定義しています。
全て準備が整ったので、検証を実施してみましょう。検証は、以下の手順で行います。なお、promelaのソースファイルは、tv.promとします。
spin -a -v tv.promすると、pan.c、pan.h、pan.b、pan.m、pan.t、というファイルが生成されます。次に、pan.cをコンパイルします。ここではgccを用いています。
gcc -DSAFETY -o tv pan.cすると、tv（Windows環境ではtv.exe）という実行形式ファイルができるはずです。早速実行してみましょう。
error: max search depth too small Depth= 9999 States= 1e+006 Transitions= 1.17922e+006 Memory= 54.539 Depth= 9999 States= 2e+006 Transitions= 2.34328e+006 Memory= 106.558 Depth= 9999 States= 3e+006 Transitions= 3.52469e+006 Memory= 158.577という表示が延々と続き、いつまでたっても終わらないようです。とりあえず実行を中断しました。spinは実行対象が取りうる全ての状態を検証するのですが、今回の対象は状態が多すぎるため、計算に時間がかかっているのが原因です。実は、spinはタイマのカウント値などの変数の値も、状態変数も、全て状態と考えて組み合わせを作り出します。基本的にタイマのカウント値は検証対象のモデルに影響を与えないはずです。そこで、タイマの上限を小さくしてみましょう。
#define OFF_TIM_MAX 2 #define ON_TIM_H_MAX 2 - 1 #define ON_TIM_M_MAX 2 - 1とりあえず、OFFタイマの設定時間を1〜2、ONタイマの設定時刻を、0:0〜1:1までに変更してみます。こうして実行すると今度は結果が出ました。
pan: assertion violated (cur_off_tim_val<=2) (at depth 4824) pan: wrote tv.prom.trail (Spin Version 4.2.7 -- 23 June 2006) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 56 byte, depth reached 4824, errors: 1 7726 states, stored 406 states, matched 8132 transitions (= stored+matched) 0 atomic steps hash conflicts: 2 (resolved) 2.929 memory usage (Mbyte)結果を見ると1行目に、assertion violated (cur_off_tim_val<=1)と表示されています。これは、検証条件を満たさない状態が存在したことを意味します。では、どんなときにこれが発生するのでしょう。それを確かめるために、-tオプションを付けてspinを実行します。
なお、tオプションは、検証で問題が発生した場合に出力されるtrailファイルを元に、実際にどのような状態変化が生じて問題に至ったのかを確認するためのオプションです。詳細は、https://www.spinroot.com/spin/Man/Manual.htmlのtrail-huntingに関する記述を参照して下さい。
spin -t tv.promを実行すると、どんな流れでassertion violatedが発生したかを表示してくれます。
spin -t tv.prom 略 STAT [S_ON :S_ON_T_NONE ] OFF TIMER SET[2] STAT [S_ON :S_ON_T_OFF ] STAT [S_ON :S_ON_T_OFF ] ON TIMER SET[1:1] STAT [S_ON :S_ON_T_OFF_ON ] OFF TIMER FIRED STAT [S_OFF :S_OFF_T_ON ] spin: line 94 "tv.prom", Error: assertion violated spin: text of failed assertion: assert((cur_off_tim_val<=2)) spin: trail ends after 4825 steps #processes: 1 s = S_OFF ss = S_OFF_T_ON queue 2 (req_power): [REQ_OFF] queue 3 (req_on_tim): [REQ_CAN,0,0] req_on_tim_val_h = 1 req_on_tim_val_m = 1 queue 4 (req_off_tim): [REQ_CAN,0] req_off_tim_val = 2 enable_on_tim = 1 cur_on_h = 0 cur_on_m = 0 set_on_h = 1 set_on_m = 1 queue 1 (is_fire_on_tim): enable_off_tim = 0 set_off_tim_val = 2 cur_off_tim_val = 3 queue 5 (is_fire_off_tim): 4825: proc 0 (main) line 318 "tv.prom" (state 256) 1 process createdassertion violatedは、OFFタイマのカウント値の条件違反を示しているので、OFFタイマを設定するところから動作を確認してみます。
- 『電源ON中-タイマセット無し』状態で、OFFタイマセット要求を受ける。設定値は2。その結果『電源ON中-OFFタイマセット中』に遷移する。
- 何もイベントが発生せず、『電源ON中-OFFタイマセット中』状態のまま。
- 『電源ON中-OFFタイマセット中』状態で、ONタイマセット要求を受ける。設定値は1:1。その結果『電源ON中-ONタイマOFFタイマセット中』に遷移する。
- 『電源ON中-ONタイマOFFタイマセット中』状態で、OFFタイマが発火する。その結果『電源ON中-ONタイマセット中』に遷移する。
OFFタイマセットからの動作は上記の通りです。そしてステップ4の終了後、cur_off_tim_valが3になっています。しかし、よく考えてみると、ステップ1でセットしたOFFタイマの設定値は2です。ということは、ステップ3でOFFタイマが発火しているはずです。発火を見落としているのでしょうか。promelaのコードを確認してみましょう（ソースコード7.1）。
ソースコード7.1.『電源ON中-OFFタイマセット中』からの遷移/* OFFタイマセット中 */ :: (ss == S_ON_T_OFF) -> if :: is_fire_off_tim?[true] -> is_fire_off_tim?_; clr_off_tim(); printf("OFF TIMER FIRED\n"); s = S_OFF; ss = S_OFF_T_NONE :: req_power?[REQ_OFF] -> req_power?_; clr_off_tim(); printf("POWER OFF\n"); s = S_OFF; ss = S_OFF_T_NONE :: req_on_tim?[REQ_SET] -> req_on_tim?_, req_on_tim_val_h, req_on_tim_val_m; set_on_tim(req_on_tim_val_h, req_on_tim_val_m); printf("ON TIMER SET[%d:%d]\n", req_on_tim_val_h, req_on_tim_val_m); ss = S_ON_T_OFF_ON :: req_off_tim?[REQ_CAN] -> req_off_tim?_, _; clr_off_tim(); ss = S_ON_T_NONE :: else -> skip fi最初のガードがOFFタイマの発火なのできちんと実装されています。一方、ONタイマの設定は3番目のガードです。それぞれ正しく実装されています。では何が起こっていたかというと、OFFタイマの発火と、ONタイマの設定というイベントが（検証対象のモデルから見て）同時に発生したため、ランダムにイベントが選択され、ONタイマの設定とそれに伴う遷移が行われていたのです。よって、OFFタイマの発火が1周期遅れ、検証条件に違反したわけです。
これは、イベントが連続して発生する限り、OFFタイマが無限に発火しないことがあり得ることを意味します。そのうちOFFタイマのカウンタがオーバーフローし、単に発火が遅れたでは済まない問題が発生するかもしれません。そして、これはレアケースではありますが現実に発生しうる問題なのです。このような、テストケースを作成するのが困難だったり、そもそもテストケースを考えつきにくい問題を発見することができるのがモデル検証の大きな利点です。
現在のモデルに問題があることは分かりましたが、修正にはいくつかのアプローチがあります。イベントに優先度を付けるアプローチ、1周期で複数のイベントを処理するアプローチ、他にもあるかもしれません。今回の問題だけをとらえるならば、OFFタイマの発火イベントを、ONタイマの設定イベントよりも優先すれば良いようにも思えますが、これでは本質的な解決になっていません。ONタイマとOFFタイマが同時に発火した場合など、どちらを優先すればよいのか困ってしまいます。もちろん、それらも含めて優先度を仕様として定めるという解決策もあります。しかし、今回は1周期で複数のイベントを処理するアプローチを取りたいと思います。この場合、1周期の処理を、処理対象のイベントが無くなるまで続けることになります。
具体的には、ソースコード8.1に示すように、前周期状態という変数を導入し、現在の状態と前周期状態が同じになるまで状態マシンを動作させ続けるわけです。当然、（promelaではなく実装言語での）実際の実装でも同じメカニズムを利用します。
ソースコード8.1.修正後の状態モデルでは、修正後のモデルを検証してみましょう。
(Spin Version 4.2.7 -- 23 June 2006) + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 60 byte, depth reached 4568, errors: 0 380698 states, stored 41976 states, matched 422674 transitions (= stored+matched) 0 atomic steps hash conflicts: 31446 (resolved) Stats on memory usage (in Megabytes): 25.887 equivalent memory usage for states (stored*(State-vector + overhead)) 21.578 actual memory usage for states (compression: 83.35%) State-vector as stored = 49 byte + 8 byte overhead 2.097 memory used for hash table (-w19) 0.320 memory used for DFS stack (-m10000) 0.074 memory lost to fragmentation 23.921 total actual memory usage unreached in proctype main line 417, state 335, "-end-" (1 of 335 states)今度は、assertion violated表示はありません。問題は解決されています。最後に、unreached in proctypeという表記があります。これは、検証対象モデルを無限ループにしているため、終了していない（終了状態に到達していない）旨を示すメッセージです。これは、意図通りですので問題ありません。もし、意図と異なり到達していない状態があれば、UMLモデルに誤りがあるか、UMLモデルをpromelaに実装する際にミスをしたと考えられます。
今回は、タイマ付きテレビを題材に、UMLモデルとpromelaコードの対応と、具体的なモデル検証方法を取り上げました。実際に作業を進める中で、分かったことをまとめると以下のようになります。
- promelaの言語要素をうまく組み合わせることで、UMLモデルからpromelaのコードを一定のルールに従って導出できました。よって仕組みさえ作れば自動化もできるでしょう。
- promelaで検証を行う際、検証の仕組み、検証対象のモデル、検証条件などを適切に分離して実装することで、可読性や変更容易性を高めることができました。
- タイマのカウント値など、検証対象のモデル以外の部分の実装を簡略化することで、検証の意味を失うことなく状態数の増加を抑制することができました
- イベントの同時発生など、気付きにくい問題を、モデル検証で発見することができました。改善した仕組みは、アーキテクチャメカニズム設計書など、適切なドキュメントに記載しておくことが重要だと思います。
本稿では、モデル検証で発生した問題のうち、特にインパクトの大きかったイベント同時発生問題を取り上げましたが、これ以外にも、電源OFF時のOFFタイマのクリアし忘れや、遷移先の誤りといった、比較的簡単なミスも次々と発見することができました。技術的に正確なたとえではありませんが、ロジックエラーがコンパイルエラーのような感覚で発見できるイメージでしょうか。今後はより複雑なターゲットへの対応などに取り組んでみたいと考えています。
なお、今回検証に用いたprolemaソースコードは、このリンク先tv.promからダウンロード可能です。
最後までご覧いただき，ありがとうございました．
- オブジェクトの広場編集部 著，『その場でつかえるしっかり学べるUML2.0』，秀和システム ，ISBN：4-7980-1239-4
| © 2007 OGIS-RI Co., Ltd. |
|
