Shoeisha Technology Media

CodeZine(コードジン)

記事種別から探す

「形式手法」の“論理の力”による開発効率と品質の向上事例

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

  • LINEで送る
  • このエントリーをはてなブックマークに追加

 社会人エンジニア向けの教育プログラム「トップエスイー」から、エンジニアの皆さんに対して有用な情報をお届けするコーナーです。ところで、形式手法という言葉はご存じでしょうか? 一般には「数理論理学に基づき、効率よく高品質なソフトウェアを開発するための手法の総称」などといわれます。とはいえ「数理論理学」といわれてもなかなか実感ができないと思います。さらに「総称」と述べましたが、セミナーや書籍などで勉強した方も、その中の一つの手法や観点のみに触れたのではないかと思います。本記事ではAmazon Web ServiceやFacebook等の具体的な事例にも触れ、形式手法と呼ばれるアプローチのいくつかの方向性・可能性について紹介します。「形式手法」という広すぎる言葉はいったん忘れて、難しい専門用語に振り回されないよう、できるだけ一般的な言葉での説明を補足します。

目次

「網羅的テストが可能な擬似コード」を用いた不具合検出

 さまざまな主体(スレッド、プロセス、機器など)が動作する並行システムでは、センサー入力など外界からのイベント、メッセージの送受信やその失敗、割り込みや故障による再起動など、たくさんの状態変化の可能性があります。また、それらの状態変化が発生する順序やタイミングも無数にあり、特定の場合のみに不具合が顕在化し問題が発生することがあります。さらに、実装したシステムを実行しても、OSのスケジューリングやネットワークの状況などにより、状態変化の順序やタイミングはその都度変わってしまいます。このため、さまざまな可能性を意図的に制御してテストしたり、不具合を再現したりすることが困難です。

 これらを考慮すると、必要なアプローチはまず、設計モデル上でさまざまな可能性をしっかりとテストすることになります。「シミュレーションする」といってもよいでしょう。とはいえ、状態変化の順序やタイミングが無数にあることが問題なので、いくつかのケースを試したとしても、一定の信頼性が担保できたとはいえません。結論として、想定したいすべての可能性を網羅的に調べる必要があることがわかります。

 これに対して、「網羅的テストが可能な擬似コード」という技術があります。ある言語で擬似コードを書くと、ツールがその擬似コードで表現されたすべての可能性を網羅的にテストするというものです。もちろん、実際にすべての可能性を試すわけではなく、さまざまな理論・技術を駆使して、それと同等のことを効率的にやってくれます。

【事例】クラウドシステムでの不具合発見

 Amazon Web Services(以下、AWS)の開発においては、この「網羅的テストが可能な擬似コード」を使っています。クラウドでは、大量のリクエスト・データを高速に、高い可用性をもって保存や処理をするため、データの複製を作ることになります。この際、データの書き込みや複製間の送受信、ノードの応答遅れやクラッシュなど、さまざまな状態変化がさまざまな順序・タイミングで発生しても大丈夫か(例えば書き込みデータが消えないか)が問題になります。そこで「網羅的テストが可能な擬似コード」を使ったわけです。実際に、擬似コード上で35ステップからなる複雑な、しかし現実的な不具合を検出したと報告されています。

 ちなみにAWSの場合は、あるチームが活用した後に、他のチーム利用に利用が広がっていったそうです。実は、「網羅的テストが可能な擬似コード」というのは、私が考えた言葉ではなく、AWS内で利用が広がっていく際に使われた言い回しです。「形式手法」や「検証」と呼ぶと遠いものに感じてしまうから、という理由で用いられた言葉とのことです。少しさびしい気もしますが、歴史的に使われてきた言葉や専門用語の印象に振り回される必要はないのですね。

【専門用語での補足】モデル検査技術

 ここで紹介した技術はモデル検査と呼ばれます。「SPIN」や「NuSMV」(ともに擬似コードの言語ではなくツールの名前)がよく知られています。Amazonで用いた擬似コードの言語は「TLA+」と呼ばれるものです。残念ながら、日本語ではあまりTLA+の情報が見つからないかもしれません。しかし、TLA+は、LaTeXの開発者であるとともに、分散システムにおける耐故障性技術の基礎を確立したことで著名なLeslie Lamport氏が開発した言語としてよく知られています。

 リスト1に、ネットワークシステムでのクライアントプログラムに対応した擬似コードの記述例を紹介します。こちらはSPINで記述しています。コメントを見れば大まかな動作は理解していただけるでしょう。

リスト1 SPINツールにおける擬似コードの例
active proctype client(){ // クライアントプロセスの例
  byte rmsg;
  bool retried = false;
  start:
  c2s ! request; // リクエストのサーバへの送信
  if
    :: s2c ? rmsg -> // サーバからの応答受信
       if // 成功か失敗かどちらかのメッセージが来て結果を記録
         :: rmsg == success -> logc = success
         :: rmsg == failure -> logc = failure
       fi
    :: timeout -> // タイムアウト時の処理
       if
         :: !retried -> // 再試行済みでなければ再試行
             retried = true; goto start
         :: else -> logc = maybefailure
       fi
  fi
}

 この「網羅的テストが可能な擬似コード」ですごいのは「網羅的テスト」をしてくれるツールのほうだと感じる方もいるでしょう。むしろ、やりたいのは「擬似コード」ではなく、プログラムコードそのものの検査と思われるかもしれません。しかし実は、網羅的テストができることは、擬似コードの大きな利点です。そして、要点が絞られ実装詳細が含まれていない擬似コードを用いる方が、本質的な問題点が抽出され、有益な結果が得られるのです。


  • LINEで送る
  • このエントリーをはてなブックマークに追加

著者プロフィール

  • 石川 冬樹(国立情報学研究所)(イシカワ フユキ)

     国立情報学研究所 コンテンツ科学研究系 准教授。電気通信大学 情報理工学研究科 客員准教授。博士(東京大学・情報理工学・2007年)。形式手法や最適化技術を中心として、ソフトウェア工学および、自律・スマートシステムのディペンダビリティに関する研究に従事。

バックナンバー

連載:トップエスイーからのアウトカム ~ ソフトウェア工学の現場から
All contents copyright © 2005-2017 Shoeisha Co., Ltd. All rights reserved. ver.1.5