ステートマシン図の設計品質の向上の一手法の紹介

著者：早水公二 (株式会社フォーマルテック)、高井利憲 (チェンジビジョン)

みなさんは、astah*で書いたステートマシン図をどのように活用していますか？システムの取り得る状態を把握したり、システムの振る舞いに関する理解を共有したり、不正な状態遷移がないかレビューしたりしていると思います。今回は、モデル検査という技術を応用することにより、ステートマシン図を自動検証する手法をご紹介します。

■モデル検査の概要

モデル検査とは、システムの網羅的な検査ができる技術です。

網羅的とはどういうことでしょうか。例えば、実機や実際の実行コードを用いる試験やソフトウェアテストでは、特定の環境条件や入力値を設定することによって、検査対象のシステムやソフトウェアの振る舞いを観察します。ただし、一回あたりの試験の実行には、無視できない時間やコストが係るため、限られた環境条件や入力値しか確かめられないのが普通です。

しかし、モデル検査では、あり得るすべての環境条件や取り得るすべての入力値に対して検査することができます。ここでは詳しく述べませんが、システムが有限状態のステートマシン図で表現できていて、かつ、試験項目や検査すべき仕様の記述が一定の条件を満たしていれば、与えられたステートマシン図の全ての実行パスでそれら試験項目や検査すべき仕様を満たしているかどうかを決定するアルゴリズムがいくつか知られており、それらを応用した技術がモデル検査技術です。ステートマシン図が有限状態といっても、ループを含む場合も当然ありうるので、実行パスの数は無数になりえますが、それでも網羅的に検査できるところがポイントです。しらみつぶしに検査するので、性質が成り立たない極めて特別な状態やパス、すなわち不具合が1つでも存在すると、必ず発見することができます。

このモデル検査を、計算機上で自動で実行するソフトウェアツールがモデル検査ツールです。この事例ではNuSMVというツールを用いました。

多くのモデル検査ツールでは検査結果が偽(false)、すなわちステートマシン図が与えられた検査項目や仕様を満たさない場合には、その証拠として反例(counter example)が出力されます。反例には初期状態から、検査項目や仕様を満たさない状態に至るまでの実行パスが示されているため、システムの動作ログと同様に順を追って解析すれば不具合の原因を究明できます。モデル検査は、不具合の発見と原因究明が同時に行える、とても有用な技術です。
モデル検査のワークフローを以下に示します。

モデル検査ワークフロー.png

モデル検査で必要な作業は二つです。一つは仕様書、設計書、ソースコードなどから「モデル」を作成する作業です。本作業は「モデル化」と呼ばれています。もう1つは、要求仕様書や試験仕様書、テスト項目などから「検査式」を作成する作業です。検査式の書き方は、モデル検査ツールごとに異なります。モデルと検査式を1つのファイルに記述してモデル検査ツールに入力します。以降の検査はツールで自動的で行われて、検査結果として、モデルが検査式を満たすことを表す「TRUE」、あるいは満たさないことを表す「FALSE」が出力されます。検査結果が「FALSE」の場合には合わせて反例が出力されます。

■検査対象のシステム

それでは、実際にモデル検査の流れを見ていきましょう。
ここでは実際の開発現場の実例に基づいた例題を紹介します。実例では、ステートマシン図の記述漏れが見つかり、それを改修することで、設計の品質が向上しました。
実例で発見された不具合は、もっと複雑なものだったのですが、ここでは、モデル検査の概要と適用の様子を分かりやすくお伝えするため、簡単な記述漏れの例題に置き換えています。

例題の「商品供給指示システム」の概要は以下の通りです。

商品供給指示システムの概要.png

商品供給指示システムのステートマシン図を以下に示します。

端末A

Terminal_A.png

端末B

Terminal_B.png

モニター

Ctl_Monitor.png

■モデルの作成

モデル検査の2つの作業のうちの1つ目です。ステートマシン図から作成したモデル(抜粋)を以下に示します。

MODULE main

VAR

   Power       : {start, ON};
   Terminal_A  : {initial, wait, send, receive, com};
   Terminal_B  : {initial, wait, send, receive, com};
   Ctl_Monitor : {initial, non_plot, surplus, sufficient, optimal, few, short};
   Event_A     : {emp,report,accept,stop_report,reject,finish_A,
                   order,response,stop_order,non_response,finish_Ctl};
   Event_B     : {emp,report,accept,stop_report,reject,finish_B,
                   order,response,stop_order,non_response,finish_Ctl};

   MD_A : -1..3;
   MD_B : -1..3;

ASSIGN

   init(Power) := start;
   next(Power) := case
     Power = start : {ON};
     TRUE : Power;
   esac;

   init(Ctl_Monitor) := initial;
   next(Ctl_Monitor) := case
     Ctl_Monitor = initial                      : non_plot;
     Ctl_Monitor = non_plot & (MD_A + MD_B = 3) : few;
     Ctl_Monitor = non_plot & (MD_A + MD_B = 1) : sufficient;
     Ctl_Monitor = non_plot & (MD_A + MD_B = 2) : optimal;
     Ctl_Monitor = non_plot & (MD_A + MD_B = 4) : short;
     Ctl_Monitor = non_plot & (MD_A + MD_B = 0) : surplus;
     TRUE : non_plot;
    esac;

モデル検査ツールNuSMVでの代表的なモデルの書き方は以下のようになります。

init(オブジェクト) := 開始状態;
next(オブジェクト) := case
  遷移条件１（トリガ & ガード）: 遷移先状態１;
  遷移条件２（トリガ & ガード）: 遷移先状態２;
　 　・
　　 ・
　　 ・
  TRUE : デフォルトの遷移先状態;
esac;

モデルはテキスト形式でコーディングします。1つのオブジェクトに対して、init()文で開始状態を定義して、next() := case・・・文で遷移条件(遷移のきっかけとなるイベントと表すトリガ、及び遷移が実施されるための必要条件を表すガード)と遷移先状態を記述します。これは、UMLのステートマシン図によっても記述できますので、モデル検査ツールNuSMVのモデルとステートマシン図はとても「相性が良い」、すなわち、ステートマシン図はモデル検査で検査しやすいと言えます。astah* のステートマシン図から、NuSMVのモデルへの変換は、岡山県立大学の横川先生が開発した自動変換ツールも公開されています (本記事の著者の一人である早水もお手伝いしております)。ご興味のある方はお試しください。
UML設計検証支援ツール：http://circuit.cse.oka-pu.ac.jp/tool.html

※2022年9月30日当ツールがダウンロードできない状況であることを確認しました。
ダウンロードご希望の方は、ご利用OS情報(Windows/Mac)と合わせて、弊社問合せフォームよりご連絡ください。

使用条件等は上記ホームページを参考にしてください。正式にはastah* community 6.7にて動作確認しています。
(他のバージョンでご利用中、不具合や不都合などございましたらご連絡ください)

■検査式の作成

次に検査式を作成します。モデル検査ツールNuSMVでは、CTL(Coputation Tree logic)式と呼ばれる論理式を用いて検査式を作成します。CTL式は、以下のような基本パターンを組み合わせて作成します。

検査式.png

事例では、たくさんの検査式を作成して様々な性質を検査しました。ここでは、不具合が発見できた検査式を紹介します。

検査式：!EF(Terminal_A = com & MD_A = 0)

Terminal_Aは従業員が持つ端末です。Terminal_A = comは通話中であることを示します。MD_Aは端末内でカウントされる変数で通話数を示します。
!EF(P)は、否定＋Exixt(存在)＋Future(将来)で「将来Pが存在しないはず」の意味です。
ここで、端末が通話中にもかかわらず通話数が0(ゼロ)という状況は有り得ないので、この検査式はTRUEとなるはずです。

作成したモデルと検査式を1つのファイルに記述して「test.smv」という名前で保存すれば、検査の準備は完了です。

■モデル検査ツールの実行と反例解析

ツールを実行してモデル検査を行います。モデル検査ツールNuSMVはコマンドラインアプリケーションなのでコマンドプロンプトで、「NuSMV test.smv」と入力して実行します。実行結果を以下に示します。
モデル検査ツールの実行と反例解析.png

検査結果はFALSEでした。Counterexample以下に反例が出力されています。反例を表形式で記述して解析します。表では必要な変数だけ日本語に変えて示しています。
イベント

ステップ3では端末が待機状態で、イベントとして従業員からの報告があります。
ステップ4では端末が発信中(報告したため)で、管理者の応答がありました。
次のステップ5が不具合の状態です。

従業員が報告のために発信して、管理者からの応答があったため端末は通話中になっているのですが、通話数が0(ゼロ)のままになってしまっています。
なぜこのような状況が発生したかと言いますと、端末Aのステートマシン図で、端末状態が発信中(send)から通話中(com)に遷移する際に、応答(response)のトリガの後に、通話数を1にするアクション(MD_A = 1)を書き忘れてしまったためです。
statemachine.png

いかがでしたでしょうか。ステートマシン図にモデル検査を適用すると、取り得る全ての実行パスを網羅的に検査できるので、起こってはいけない状況や振る舞い、ガードやアクションの記述ミスや記述漏れを必ず発見することができます。

また、上で紹介したとおり、astah*のステートマシン図からNuSMVのモデルへは、自動変換できるツールも公開されています。
UML設計検証支援ツール: http://circuit.cse.oka-pu.ac.jp/tool.html

※2020年3月16日
当ツールがダウンロードできない状況であることを確認しました。現在状況を確認中です

※2022年9月30日
ダウンロードご希望の方は、弊社問合せフォームよりご連絡ください。
ご利用OS情報(Windows/Mac)を合わせてご連絡ください。

モデル検査は、適切に活用すれば非常に強力な技術です。astah* で記述したステートマシン図の新しい活用法として検討してみてください。

■謝辞

本記事の執筆にあたっては、岡山県立大学の横川智教先生にご協力いただきました。
ありがとうございました。

コメントを残す

以下に詳細を記入するか、アイコンをクリックしてログインしてください。

Gravatar
WordPress.com ロゴ

WordPress.com アカウントを使ってコメントしています。 ( ログアウト /  変更 )

Facebook の写真

Facebook アカウントを使ってコメントしています。 ( ログアウト /  変更 )

キャンセル

%s と連携中