作成したモデルの検査結果
先の検査式1から8を表5の環境にて検査しました。検査時間と状態数は表6に示す通りです。
| メモリ | 16GB |
|---|---|
| CPU | Intel Core(TM) i7-3770K |
| OS | Windows(R) 7 |
| 検査式 | 状態数(百万) | 所要時間（秒） |
|---|---|---|
| 1 | 5790 | 406000 |
| 2 | 58 | 114 |
| 3 | 77 | 151 |
| 4 | 74 | 172 |
| 5 | 37 | 82 |
| 7 | 162 | 329 |
| 8 | 162 | 321 |
この検査の結果、反例が見つかりました。それは、通信ロスにより、ブラウザ側のリビジョン番号がサーバー側のリビジョン番号を下回った状態（同期未完了の状態）にも関わらず、サーバーの認証済みリビジョン番号がリビジョン番号と等しくなる場合があることです。この場合、サーバーは状態の更新要求や更新承認を出さないため、ブラウザは更新要求を出し続けるループに陥ります。さらに調査した結果、この反例に対応するループが実際の同期処理コード上でも発生することが判明したため、同期処理コードとPromelaの両者に修正を行いました。修正の結果、反例が示されなくなったことを確認できました。
この反例は、通信ロスに起因するものでしたが、パケットロス率［1］を1～5％とし、監視制御システムでの秒間メッセージ数を1ユーザーあたり0.05回／秒程度と見積もると、年間約1回から40回発生した可能性があると試算できます。また、一度この状態に陥った場合、ループから抜けるためにはブラウザまたはサーバーの再起動が必要なため、致命的な問題であったと考えられます。開発環境やテストで発見されなかった理由としては、次の3点が考えられます。
- WebSocketやLong polling通信における断続的な切断に対処するためのPiggyback（後述）による効果
- 開発環境におけるメッセージロス率の低さ
- 高確率でメッセージロスを発生させた場合、接続済み状態にすら到達しにくく、問題箇所に至らない
Piggybackとは複数の隣接するメッセージを同時に送信する方法ですが、このPiggybackにより、問題の反例を発生させるメッセージロス以外のロスが同時に発生することとなり、反例を見えにくくしていました。また、開発環境におけるメッセージロス率を人為的に上げた場合は、反例を発生させる状態まで到達しておらず、問題の箇所をテストできていなかったと考えられます。Promela上で示された反例に対し、実コード上での対応部分を容易に発見できたのは、Promelaが実コードに近く記述されていたためで、Spinの良さの1つといえます。
参照
［1］: N. Taft, F. Ricciato, Comparison of User Traffic Characteristics on Mobile-Access versus Fixed-Access Networks, PAM 2012, LNCS 7192, pp. 32-41, 20
おわりに
今回はWebベースの監視制御システムにおける状態同期の信頼性について、Spinを用いたモデル検査を行いました。その結果、従来使用していたテストでは検出されないシステムを停止させる実行パスを検出することができました。この反例は、実際の同期処理コードでも再現し、もしこの反例が発現した場合は再起動が必要となるという致命的なものでした。この不具合は、開発環境での通信路上のメッセージロス率や通信の特性上、開発時には発見できなかったと考えられ、モデル検査による検査が有効であったといえます。全ての開発でここまで検査に工数を割くことは難しいと思いますが、通信が含まれるなどの不確実性が高くかつ重要なコードについては、積極的なモデル検査の活用が近道であると考えています。
トップエスイーについて
「トップエスイー」は、国立情報学研究所で提供している、社会人エンジニア向けのソフトウェア工学に関する教育プログラムです。トップエスイーでは講義や制作課題を通して、最先端の研究成果や現場で得られた知見が蓄積されてきました。その「アウトカム」、つまり成果やそこに至る過程を紹介し、現場のエンジニアの方々に活用していただける記事を連載しています。昨年まで実施していた修了制作の成果を今回の記事で紹介しました。修了制作は本年度より、アドバンスコースのプロフェッショナルスタディや、トップエスイーコースのソフトウェア開発実践演習へと形態が変わりましたが、受講者の周辺で発生した問題点を自分で解決することに取り組むことは、単独での展開からグループ作業など多彩な展開ができるカリキュラムへと進化しています。
