システムの網羅的なテストができるモデル検査
実課題を扱ったモデル検査のコンテスト「MoCCon」を振り返る

トップエスイーからのアウトカム ～ ソフトウェア工学の現場から 第4回

実際の適用事例を基にした競技課題

　モデルチェッキングコンテストで示された課題の最大の特徴は、国内のメーカーで実際にモデル検査を用いて検査業務を行った適用事例を基にしたことです。事例では、出荷直前のシステムで発生した不具合の原因について、モデル検査を用いて究明しました。

　コンテストで出題された課題（問題と背景および提出物）の原文を表6に示します。不具合は実際の適用事例で発見したものを基にあらかじめ仕込んであります。

表6　競技課題

問題
通信端末の上位側の仕様書と詳細設計書を提示。
試運用中に1度だけ、着信履歴数が10000件に達してしまう不具合が発生した。
その原因をモデル検査を用いて調査せよ。
背景
開発部門から不具合原因の調査を依頼された。
開発部門は多忙で質問不可のため、適宜、仮定や前提を自分で定義する。
開発部門はモデル検査の知識は一切ない。
提出物：モデル検査報告書
提出先は開発部門（依頼者）。
開発部門が理解しやすいよう工夫すること。

　今回の検査対象はキャッチホンの機能が付いた通信端末のシステムです。コンテストの応募者は日本語で書かれた上位側の仕様書（機能仕様書）（表7）と、状態遷移表で設計された詳細設計書を入手することができます。

　応募者は、機能仕様書を読んで通信端末のシステムの振る舞いを理解します。次に、入手した2つの状態遷移表をモデル化します。必要に応じて抽象化と絞り込みの工夫が必要です。

表7　機能仕様書

機能仕様書
他の複数の端末と通話を行うための通信端末である。
同時に2回線（現通話＋他端末からのキャッチホン）の通話ができる。
自端末からの発信は待機中のみ可能である。
他端末が応答する前であれば発信を中止できる。
他端末が応答した場合は通話が成立する。他端末が応答を拒否した場合は通話は成立しない。
他端末が応答を拒否した場合は他拒否履歴を保存する。
自端末が待機中であれば他端末からの着信を受け付ける。
他端末からの着信を受け付けた場合は着信履歴を保存する。
また、自端末が通話中だがキャッチホンを受けていない状態であれば他端末からの着信を受け付ける。
他端末からの着信に対して応答または拒否することができる。
自端末で応答した場合は通話が成立する。自端末で応答を拒否した場合は通話は成立しない。
自端末で応答を拒否した場合は自拒否履歴を保存する。
本機種では履歴保存用メモリの容量が小さいため以下の処理を行う。
着信履歴は 10000件まで保存可能であるが、5000件ごとにバックアップを実施した上でリセットする。
自拒否履歴は3000件まで保存可能であるが、1500件ごとにバックアップを実施した上でリセットする。
他拒否履歴は1800件まで保存可能であるが、 900件ごとにバックアップを実施した上でリセットする。

　次に、入手した2つの状態遷移表をモデル化します。状態遷移表は表9と表10で、表の1行目に状態、左側には操作が記述されています。操作と応答の交差するセルは上下の2行からなり、上の行は遷移先の状態、下の行は実行される処理（アクション）を示します。例えば3列目の「CHAKU」は着信してコールしている状態を示し、その状態の時に2つ目の操作である「a_outou」が発生したとします。つまり着信に応答することで、CHAKUとa_outouの交差するセルに記述されている通り「TSUWA」という状態、すなわち通話に移行することを意味しています。その時、接続している端末数を示す変数mtxの値を増加させています。

表8　状態遷移表（送受信装置）

表9　状態遷移表（リセット装置）

　端末内に配置された送受信装置とリセット装置は並行して動作するため、そのようにモデルを作成します。リセットするものは着信履歴と自拒否履歴、他拒否履歴の3つがありますが、リセット信号（reset）は1つだけです。少し改良したくなる仕様ですが、モデル化では元のシステムを忠実に再現してモデルを作成します。

　最後に、検査式を作成して検査を行います。モデル化がうまくできていて正しい検査式が書けていれば、不具合の原因を究明することができます。検査式の例としては以下が挙げられます。

検査式：!EF(着信履歴数 = 10000)

　検査式の意味は「将来（Future）、着信履歴数が10000件に達することはない（!Exist）はずである」となります。検査結果がFALSEの場合には、着信履歴数が10000件に到達するまでのパスが反例で出力され、不具合の原因を究明することができます。

不具合の原因

　本稿で前述した「リセットするものは3つだがリセット信号は1つだけ」という説明は、モデル化における不具合につながるヒントです。しかしながら、実際のコンテストではこういったヒントは示していません。競技者は仕様書と設計書をよく読んで、システムの特徴を理解する必要があります。

　さて、気になる解答、すなわち不具合の原因は、このリセット信号の排他制御ができていないミスということになります。必要な検査式が全て記述され、モデル検査で妥当な検査ができる状態になっていれば、表10のようなパスが反例として出力されます。状態遷移表にある操作b_hatsuなどのアクションにあるように、実際の処理は履歴の値を調べてリセット装置のフラグresetをTrueにし、その後に履歴の値を1だけ増加しています。そのため、5000件目のアクションを行う時には履歴の数値は4999となります。2つの状態遷移表と合わせて見れば不具合の原因が分かります。なお、正解となるモデルコードと検査式については非公開としています。

表10　不具合の原因

1．	初期状態は端末は待機状態で全ての履歴は0件である。
2．	端末の操作を繰り返すうちに以下のような状態となる。 着信履歴が4997件 自拒否履歴が1498件
3．	他端末から自端末に着信があり着信履歴が4998件となる。
4．	着信を拒否することで自拒否履歴が1499件となる。
5．	自拒否履歴のリセットとバックアップのためにリセット信号をONにする。
6．	リセット装置で自拒否履歴のリセットとバックアップを開始する。
7．	再度、他端末から自端末に着信があり着信履歴が4999件となる。
8．	着信履歴のリセットとバックアップのためにリセット信号をONにする。 （ただし、リセット信号は5．で既にONとなっているため、ここでは維持となる。）
9．	ここで自拒否履歴のリセットとバックアップが完了してリセット信号がOFFとなってしまう。
10．	リセット信号がOFFのため着信履歴のリセットとバックアップが行われない。
11．	他端末からの着信が継続して発生し、着信履歴が10000件に到達してしまう。

　読者の中には状態遷移表をじっくり見て、リセット信号が怪しいと気付かれた方もいるかもしれませんが、ただ怪しいだけでは不具合の原因究明にはなりません。モデル検査を用いて検査すると、反例によって端末の状態の変化や履歴数の変化、リセット信号の振る舞いなど、初期状態から不具合に至るまでのパス、すなわちシステムの振る舞いが明確に示されるので、不具合の詳細な原因究明を行うことができます。

おわりに

　モデル検査は、これまで困難といわれていたシステムの網羅的な検査ができるだけでなく、不具合を発見した場合には、その状態に到達するまでのパスを反例として得られるので、不具合発見と同時に原因を究明することができるとても有用な技術です。世の中のあらゆるものがインターネットでつながるIoTの世界では、1つのシステムの不具合が社会全体に影響を及ぼすため、個々のシステムの品質がとても重要になってきます。網羅的な検査によって不具合を徹底的に見つけて品質を向上させるモデル検査の技術が、今後さらに利用され、産業界で普及することが望まれます。なお、2回目のモデルチェッキングコンテストは2017年の8月に開催される予定です。この記事を読んでモデル検査に興味を持ったエンジニアからの応募を期待しています。

トップエスイーについて

　「トップエスイー」は、国立情報学研究所で提供している、社会人エンジニア向けのソフトウェア工学に関する教育プログラムです。トップエスイーでは講義や制作課題を通して、最先端の研究成果や現場で得られた知見が蓄積されてきました。その「アウトカム」、つまり成果やそこに至る過程を紹介し、現場のエンジニアの方々に活用していただける記事を連載しています。形式手法や今回紹介したモデル検査について、トップエスイーでは基礎的な理論から実現場での応用まで幅広い講義を用意しています。また、これまでの修了制作でも多くの受講生がモデル検査に取り組んできています。記事で紹介したコンテストの課題のように、一見するとどこに問題点があるのか分からない状況でも答えを導き出す高い検出力を発揮することもあります。2017年の8月に開催される次回のMoCConに向けて、モデル検査のマスターにチャレンジしてみてはいかがでしょうか？ じっくり学習するにはトップエスイーの受講をお勧めします。