実装モデル検証

 

平成24年度シラバス

 

 

 

 

 

 

 

 

 

 

 

 

２０１2年１月１３日

 

 

国立情報学研究所

トップエスイープロジェクト

代表者　本位田　真一

 

1.     講座名

実装モデル検証

 

2.     担当者

田辺　良則、Cyrille Artho

 

3.     本講座の目的

本講座では、ソフトウェアプログラムの検証問題を扱う。ネットワークを介したメッセージ通信を通して動作する分散ソフトウェアの振る舞いを網羅的に検証する技術、および計算機上で扱える程度の規模に検証問題を変換する抽象化技術を習得する。具体的には、Javaプログラムのモデル検査ツールJava PathFinderを使用し、実際のシステム開発に適用する方法を習得する。講義を通してモデル検査技術の理解を深め、実問題への適用能力を体得できる効果が期待できる。

 

4.     本講座のオリジナリティ

Java PathFinderなどのソフトウェアプログラムのモデル検査ツールを使用した検証については、従来多くの同様な講座が開講されている。しかしそれらの講座には後述する問題点があったため、受講生が習得した内容を速やかに開発現場で適用するための障害となっていた。本講座では、問題点を解消し、本講座受講後Java PathFinderツールを速やかに開発現場で適用できるように配慮している。

表 1に、既存の講座の問題点と、本講座における解を示す。

 

 

表 1 既存の講座の問題点と、本講座における解

既存の講座の問題点

本講座における解

現実的なシステムのプログラムは、通常GUIや通信機能のための標準ライブラリを使用しているが、この場合、そのままではJava PathFinderを使用して検証することができないため、そのようなライブラリを使用しない、簡単なプログラムしか扱っておらず、習得した内容を、実際のシステム開発に適用するのが難しい。

現実的なシステムのプログラムの検証に必要な、複数プロセスのプログラムを1プロセスのものに変換するノウハウ、また抽象化によりライブラリを使用しないプログラムに変換するノウハウを習得するので、実際のシステム開発にも容易に適用可能である。

 

5.     本講座で扱う難しさ

近年、ソフトウェアの大規模化、複雑化が進んでいる。典型的な例として、家電の制御ソフトウェアを考えると、複数の家電機器がネットワークに接続され、相互に連携して動作することで1つの機能を実現する、ネットワーク家電製品の市場が急速に立ち上がりつつある。従来の家電機器の制御ソフトウェアは単体で動作するように実装されており、単体での試験の実施が比較的容易であった。一方、ネットワーク家電では、他の機器との連携動作のためのプロトコルが組み込まれた分散処理型の制御ソフトウェアが中心的役割を担う。ホームネットワークに接続される機器やインターネット上のサービスとの接続関係を常に監視し、時折発生する接続要求や不慮の接続エラーなどに迅速かつ安全に対応できる機能が搭載されていなければならない。このように、大規模化に合わせて、ソフトウェアの安全性に対する要求も高くなっている。ところが現実には、ソフトウェア規模の増大につれ、相互作用の振る舞いが複雑になってしまうなどの原因により、綿密にプログラムを設計したとしても、機器間で資源を奪い合う競合状態のような、論理的に安全でない状態がプログラムの中に混入してしまう可能性が増大している。ソフトウェアの全動作パターンを人手で検証する従来型のソフトウェア試験は、膨大な工数を必要とするために、もはや現実的な手段ではなくなってきている。さらに、分散ソフトウェアの場合、ネットワークを介したメッセージ通信を通して相互作用を行うが、従来の試験ではソフトウェアの外部からメッセージの交換順序等を制御することは容易ではないため、振る舞いを網羅的に試験できてはいないのが実状である。

 

6.     本講座で習得する技術

本講座は、Java言語で実装された分散ソフトウェアプログラムに対するソースコードモデル検査技術を扱う。モデル検査器はJava PathFinderを用い、このモデル検査器特有のノウハウと、一般のソースコードモデル検査技術の両方が身につくようにする。対象とするプログラムは、主として並行動作を行うものであり、そのようなプログラムの安全性および活性を検証することができるようになる。さらには、異なるJava VM上で動作する複数のプログラムが、ネットワークを介したメッセージ通信により相互作用を行う、分散処理型のソフトウェアまでをカバーする。これには、分散ソフトウェアが利用する通信ライブラリを適切に置換することによって、単一Java VM上の並行ソフトウェアへと変換する技術が含まれる。また、一般にモデル検査においては、状態爆発と呼ばれる、検証のための探索空間が巨大になってしまう問題への対処が重要であるが、本講座で扱うソースコードモデル検査では、特にこの問題が生じやすい。これに対処するための，探索空間を縮減する手法も習得する。

7.     前提知識

本講座の受講生は、以下の項目を習得済みであることが望ましい。

・   Javaプログラミング

Ø  ソケットを使用した通信プログラミングを含む

・   以下に関する基礎理論

Ø  並行プログラム：非決定性、資源共有・排他制御、通信、安全性、生存性、公平性

Ø  状態探索手法：深さ優先探索、幅優先探索

・   モデル検査技術の原理

Ø  時相論理：構文、意味論(Kripke構造)、パターン(安全性、生存性など)

Ø  遷移系とその抽象化：データ抽象化

なお、これらの項目のうちJavaプログラミング以外は、全て「基礎理論」講座で習得可能である。

8.     講義計画

 

  第1回から第9回までの講義は日本語で，第10回から第15回までの講義は英語で行われる．英語の講義に際しては，日本人講師が，演習を中心として言語面でのサポートを行う．

 

・   概要

第1回：概論とツール紹介

第2回：JPF検証における基本技法

第3回：ソフトウェアの安全性検証(1)

第4回：ソフトウェアの安全性検証(2)

第5回：ソフトウェアの活性検証(1)

第6回：ソフトウェアの活性検証(2)

第7回：スケジューリングの公平性

第8回：抽象化

第9回：グループ演習

第10回：ネットワークソフトウェアの検証の難しさとその解法（概論）

第11回：centralizationモデルによる white-box アプローチ

第12回：cacheモデルによる black-box アプローチ

第13回：linear cache

第14回：branching cache

第15回：グループ演習

 

・   詳細

第1回：概論とツール紹介

Ø  問題提起

²  ソフトウェア開発における課題

²  モデル検査の位置づけ

Ø  ソフトウェア開発におけるモデル検査技術の活用

Ø  ツール紹介

²  JPF、他

Ø  演習

第2回：JPF検証における基本検証技法

Ø  Java基本事項の復習

Ø  デッドロックの検出

Ø  アサーションの検証

Ø  演習

第3-4回：安全性検証

Ø  ユーザ定義プロパティ

Ø  VMリスナー

Ø  サーチリスナー

Ø  演習

第5-6回：活性検証(1)

Ø  活性の表現とLTL

Ø  弱い公平性と強い公平性

Ø  排他制御と活性

Ø  演習

第7-8回：スケーラビリティ

Ø  半順序簡約

Ø  JPFにおける半順序簡約と到達可能性

Ø  状態空間の縮約

Ø  選択生成器

Ø  Model Java Interface

第9回：グループ演習

Ø  並行プログラムに対するモデル検査

Ø  2人または3人による発表

Ø  質疑応答および講評

第10回：ネットワークソフトウェアの検証の難しさとその解法(概論)

Ø  外部プロセスのスタブ化

Ø  ロールバック

Ø  演習問題

²  Daytime server

第11回：centralizationモデルによる white-box アプローチ

Ø  単一VM上のマルチスレッド化

Ø  演習

第12回：cacheモデルによる black-box アプローチ

Ø  Centralizationでは扱えない問題に対する解法

Ø  演習

第13回：linear cache

Ø  メッセージ交換が決定的である場合のモデル検査技法

Ø  演習

第14回：branching cache

Ø  メッセージ交換が非決定的である場合のモデル検査技法

Ø  演習

第15回

Ø  グループ演習

²  ネットワークプログラムに対するモデル検査

²  2人または3人による発表

²  質疑応答および講評

9.     教育効果

本講座を受講することにより、実際のシステム開発、特にネットワークソフトウェアの開発に適用可能な、ソフトウェアプログラム検証手法を習得できる。その結果、開発現場において、モデル検査ツールを活用することにより、信頼性の高いシステムを、効率的に開発することができるようになる。

 

10.  使用ツール

Java PathFinder：Javaプログラムのモデル検査ツール

・   使用する上での難しさ

Ø  複数プロセスで動作したり、通常GUIや通信機能のための標準ライブラリを使用したりしているような、現実的なプログラムの検証が難しい

Ø  検証項目の表現が難しい

Ø  検証の結果がエラーの場合、反例をプログラム修正に反映するのが難しい

・   使用上必要なノウハウ

Ø  通信のcentralization

Ø  ライブラリ抽象化

Ø  検証項目表現

²  安全性表現ノウハウ

²  活性表現ノウハウ

Ø  反例分析

・   選択理由、実用性：実用性が最も高いJavaプログラムのモデル検査ツール

 

11.  実験及び演習

規模の小さなものから複雑な問題へと順に取り組むことによって、モデル検査技術を段階的に体得する。まず、並行ソフトウェアに対する検証問題を通して、モデル検査技術の基本的素養を学ぶ。次に，分散ソフトウェアに対する検証問題を通して抽象化技術を習得し、モデル検査技術の現実問題への適用能力を養う。

 

12.  評価

演習課題レポート、プレゼン発表、出席日数を総合して評価する。

13.  教科書/参考書

·           B. Berard, et al, “Systems and Software Verification: Model-Checking Techniques and Tools,” Springer Verlag, 2001.

モデル検査手法を利用したソフトウェア検証について、入門から実践までの一通りが述べられており、この講義に最適である。

 

·           E. M. Clarke, et. al, “Model Checking,” MIT Press, 2000.

モデル検査手法の原理を理論的に述べたものであり、上記教科書を補うのに最適である。

 

·           W. Visser, et. al. “Model checking programs,” Automated Software Engineering Journal, vol.10, num.2, 2003.

 

·           F. Lerda and W. Visser. “Addressing dynamic issues of program model checking,” Proceedings of SPIN2001, 2001.

モデル検査ツールJava PathFinderの原理を理論的に述べたものであり、上記教科書を補うのに最適である。