トップエスイー講座「並行システムの検証と実装」　（2007〜2014）
磯部祥尚　（産総研＆情 報研）

ここでは、国立情報学研究所で磯部が担当していたトップエスイー講座「並行システムの検証と実装」について補足します。本講座のシラ バスはここからダウンロードできます。この講座ではプロセス代数CSPをベースに、並行システムをモデル検査器FDRで検証し、JavaライブラリJCSPで実装す る方法を講義しています。参考までに、2011年の講義で使用した「まえがき」のテキストとスライドをここに置いておきます（preface-text.pdf ,  preface-slide.pdf）

news: 本講座のテキスト「並行システムの検証と実装」が近代科学社から出版されました（2012.12.26）
news: 本テキストの情報（サンプルコードのダウンロードなど）はこちらをご覧ください。





以下、本講義で使用する　JavaライブラリJCSP　と　モデル検査器FDR（と その補助ツール TypeChecker, ProBE） 　のインストール方法を説明します。尚、FDRはLinux上で動作するため、Windows上にLinux環境を比較的簡単に構築する方法も説明してい ます（VirtulBox + Ubuntu）。

JCSP 開発版のインストール
[概要]

JCSP はJavaでCSPプロセスモデルを実装するためのライブラリである。ここでは、Windows にJCSPをインストールする方法を説明する。JCSPはオープンソース（LGPL licence）であり、バイナリとソースの両方を無料でダウンロードできる。JCSPは現在も開発が続けられており、現在（2011年8月24日）の最 新版はバージョンは1.1である。

[基本情報]

開発元 University of Kent
バージョン JCSP 1.1 (開発版)
Web
http://www.cs.kent.ac.uk/projects/ofa/jcsp/
備考
 Lesser GPL　（詳しくはここを読んで）

[ダウンロード]

JCSPのバイナリファイルは、ケント大学のウェブページ から JCSP 1.1 Release Candidate 4 をダウンロードすることができるが、このバージョン（jcsp-1.1-rc4）は古いため、ネットワークチャネルのパッケージ （org.jcsp.net2）が含まれていない。ここから最新のソースファイルをダウンロードして、バイナリファイルをビルドすることもできるが、ここ では、別のウェブページからバージョン（jcsp-1.1-rc5）のバイナリファイルをインストール方法を説明する。

[インストール手順]
  1. Maven Hubのウェブページ（The JCSP Library - jcsp-1.1-rc5）を開き、このウェブページ中の項目Files:にあるjcsp-1.1-rc5.jar をダウンロードして適当なフォルダに保存する。ここでは、C:\java\jcsp のフォルダに保存したとする。

  2. 環境変数CLASSPATH に
    　　C:\java\jcsp\jcsp-1.1-rc5.jar
    を 追加する。Windows 7の場合、環境変数を設定するパネルは次の手順で開くことができる： [コントロールパネル] → [システムとセキュリティ] → [システム] → [システムの詳細設定] → [詳細設定] → [環境変数]。CLASSPATHがない場合は新規に作成する。このとき、次のようにカレントフォルダも追加しておく：
    　　.;C:\java\jcsp\jcsp-1.1-rc5.jar
    先頭にドットとセミコロン（.;）が付いていることに注意。

  3. 必須ではないが、jcsp-1.1-rc5.jarと同じフォルダ（C:\java\jcsp）に、JCSPのノードサーバを起動するためのファイル（TCTIPNodeServer.bat）をダウンロードして置いておくと便利。

  4. 必須ではないが、ケント大学のウェブページ から最新のソースコードをダウンロードしておくと便利。次のsvnコマンドでソースコードのすべてのファイルを（コマンドを実行したフォルダに）ダウンロードできる。

       svn checkout http://projects.cs.kent.ac.uk/projects/jcsp/svn/jcsp/trunk/

[動作確認]
  1. メッセージボード（ネットワーク版）の例を使って動作を確認する。下記のファイルを適当なフォルダにダウンロードして展開する。

    　　MessageBoard.zip  (14KB)   [2009.11.26更新]

  2. MessageBoard\src フォルダの下の build.bat をダブルクリックしてビルドする。

  3. MessageBoard\bin\MessageBoard フォルダの下にclassファイルが生成されていることを確認する。

  4. JCSPをインストールしたフォルダ（例： C:\java\jcsp）を開き、その中の

    　　TCTIPNodeServer.bat

    をダブルクリックしてJCSPのノードサーバを起動する。または、このフォルダで、

    　　java org.jcsp.net2.tcpip.TCPIPNodeServer

    を実行して起動する。このとき、ファイアウォール等が起動確認をすることがあるが、許可する。

  5. MessageBoard\bin フォルダに戻り、server.bat をダブルクリックして起動する。ノードサーバのIPアドレスを聞かれるが、何も入力せずに[ENTER]でよい（ノードサーバが別のPCで起動している場 合はそのIPアドレスを入力する）。「サーバ稼働中」と表示される。

  6. 同様に client.bat をダブルクリックしてクライアントを起動する（IPアドレスはENTER）。[接続]をクリックし、下の[入力]欄に適当なメッセージを入力し、緑色の メッセージボードを左クリックするとそのメッセージが表示される。

  7. そのまま再び client.bat をダブルクリックして別のクライアントを起動する（複数可）。[接続]をクリックし、メッセージボードにマウスを移動すると初めのクライアントと同じメッ セージが表示される。

  8. メッセージの左端にマウスポインタを合わせると文字が赤くなるので、ドラッグで移動、右クリックで削除ができる。

  9. 他のPCにクライアントを起動することもできる。クライアントを他のPCに起動した場合は、起動時にノードサーバが稼働している PCのIPアドレス（例： 150.29.xxx.xxx） を入力する。

  10. クライアントは[切断]後に閉じるボタン[×]で終了する。接続中に[×]を押すとサーバがタイムアウトするまで（約10秒間） 全てのクライアントの動作が固まるが、タイムアウト後に復帰する。

MessageBoardスナップショット


FDR のインストール
[概要]

FDR はFormal Systems (Europe) Ltd (http://www.fsel.com/) から販売されているCSPのモデル検査器である。アカデミック目的であれば無料で使用できる。Windows 版はないため、Linux用のFDRをインストールする。Linux環境の構築例は後で紹介する。

[基本情報]
開発元 Formal Systems (Europe) LTD.
バージョン FDR2.94 academic release
OS Linux
Web
http://www.fsel.com/
備考
 アカデミック目的でのみ無料（注意）


[インストール手順]
  1. FDR2 のページ(http://www.fsel.com/fdr2_download.html) を開き、アカデミックユースの無料版をダウンロードするために、[FDR 2.94 Academic use binaries verbatim] をクリックすると、オクスフォード大学のウェブページが開く。

  2. Solaris用、Linux（32bit, 64bit）用、OSX用のバイナリファイルが用意されているので、OSにあったファイルをダウン ロードする。ここでは、Linux用（32bit版）で説明する。まず、fdr-2.94-academic-linux32.tar.gz をダウンロードし、適当はディレクトリ（例えば ~/download ）に保存する。

  3. fdr-2.94-academic-linux32.tar.gz をダウンロードしたディレクトリ(~/download) に移動し、適当なディレクトリ（例えば~/tool）に展開する（rootディレクトリではない方がよい）。

    　　tar -C ~/tool -zxvf  fdr-2.94-academic-linux32.tar.gz

  4. 環境変数 FDRHOME を FDR をインストールしたディレクトリにセットし、FDR を起動するコマンド fdr2 を PATH に追加する。例えば、.bashrc に次の 2 行を追加する。

    　　export FDRHOME="$HOME/tool/    fdr-2.94-academic-linux32"
    　　PATH="$FDRHOME/bin:$PATH"
[動作確 認]
  1. FDRのサンプルファイルが入っているディレクトリ$FDRHOME/demo/に移動し、mbuff.cspを読み 込みながらFDR を起動する。

    　　fdr2 mbuff.csp

  2. FDR 本体のウィンドウの中に "? SPEC [FD= SYSTEM" という項目あるので、この部分をダブルクリックするとSYSTEM がSPEC の詳細化であるかが検証され、?がチェックになることが確認できる。

  3. メニューの[FILE] から[EXIT] を選んで終了する。

[補足事項]
  1. FDR2-9のマニュアル（PDF版）は下記から入手できる

             http://www.cs.ox.ac.uk/projects/concurrency-tools/download/fdr2manual-2.94.pdf

    少し古いFDR2-8のマニュアル（HTML版、PS版、PDF版）は下記から入手できる

             http://www.fsel.com/fdr2_manual.html

  2. 参考までに上記のJCSPの動作確認時に紹介したメッセージボードのFDRスクリプトをここに置いておく。

    　　　　MessageBoard.fdr2     [2009.11.26更新]


TypeChecker のインストール
[概要]

TypeCheckerはFDR記述内に構文エラーがないかを検査するツールである。FDRは構文検査機能が弱いため、FDRで読込む前にchecker で検査した方が良い。

[基本情報]

開発元 Formal Systems (Europe) LTD.
バージョン  checker-beta4.linux6
OS Linux （Fedora 6, 10, 11, Ubuntu 8, SLAX6で動作確認済）
Web
http://www.fsel.com/
備考
 無料で利用可


[インストール手順]
  1. Type Checkerのページ(http://www.fsel.com/typechecker_download.html) を開き、TypecheckerのIntel (x86) architectureのLinux版(checker-beta4.linux6.tar.gz)を適当なディレクトリ(例えば ~/download) にダウンロードする。

  2. FDRをインストールしたディレクトリにcheckerというディレクトリを作成する。

    　　mkdir $FDRHOME/checker

  3. checker-beta4.linux6.tar.gz をダウンロードしたディレクトリ(~/download) に移動し、2で作成したディレクトリに展開する。

    　　tar -C $FDRHOME/checker -zxvf checker-beta4.linux6.tar.gz

  4. ディレクトリ $FDRHOME/bin に移動し、次のシンボリックリンクを作成する。

    　　ln -s ../checker/checker checker
[動作確認]
  1. FDRのサンプルファイルが入っているディレクトリ$FDRHOME/demo/に移動し、mbuff.cspnの構文をチェッ クする。

    　　checker mbuff.csp

  2. 次のメッセージが表示されれば成功。

    　　CSP TypeChecker Beta release 4. (c) Formal Systems (Europe) Ltd.
    　　CSP script is type correct.


ProBE のインストール
[概要]

ProBE はFDR記述中の各プロセスの動作を1 ステップ毎に確認するツールである。

[基本情報]

開発元 Formal Systems (Europe) LTD.
バージョン probe-1.30-linux6
OS Linux （Fedora 6, 10, 11, Ubuntu 8, SLAX6で動作確認済）
Web
http://www.fsel.com/
備考
 無料で利用可


[インストール手順]
  1. ProBEのページ(http://www.fsel.com/probe_download.html) を開き、ProBEのLinux版(probe-1.30-linux6.tar.gz)を適当なディレクトリ(例えば~/download) にダウンロードする。

  2. probe-1.30-linux6.tar.gz をダウンロードしたディレクトリ(~/download) に移動しFDRのディレクトリに展開する。

    　　tar -C $FDRHOME -zxvf probe-1.30-linux6.tar.gz

  3. ディレクトリ $FDRHOME/bin に移動し、次のシンボリックリンクを作成する。

    　　ln -s ../probe-1.30-linux6/probe probe
[動作確認]
  1. FDRのサンプルファイルが入っているディレクトリ$FDRHOME/demo/に移動し、mbuff.cspnの動作をチェッ クするためのウィンドウを起動する。

    　　probe mbuff.csp

  2. 次のウィンドウが表示されれば成功。


     
  3. SpecをダブルクリックするとSpecの動作をチェックするための別のウィンドウが起動する。



Linux 環境の構築例　（VirtualBox + Ubuntu）
[概要]

Linux 環境を構築するには様々な方法があるが、ここでは比較的簡単かつ無料で構築できる方法として、仮想環境VirtualBoxにLinux Ubuntu をインストールする方法を紹介する。尚、使われているPCに依存してここに書かれているとおりにいかない場合もある。VirtualBoxやUbuntu についての多くの情報は web 上から得ることができるので、そちらも参考にしてほしい。

[基本情報]

VirtualBox
開発元 ORACLE
バージョン VirtualBox 4.1.20 for Windows hosts
OS Windows
Web
http://www.virtualbox.org/
備考
 無償


Ubuntu
開発元
 Ubuntu Japanese Team
バージョン
 ubuntu-ja-10.04.3-desktop-i386
OS
 VirtualBox用
Web
 http://www.ubuntulinux.jp/
備考
 無償


[インストール手順]
  1. VirtualBoxのダウンロードのページ(http://www.virtualbox.org/wiki/Downloads) からWindows版

    　　VirtualBox 4.3.12 for Windows hosts (x86/amd64) 　　　（最新版 4.3.14 の動作は未確認）

    をダウンロードして実行する。後はインストーラに従う。

  2. Ubuntuは VirtualBox用の仮想ハードディスクイメージが既に用意されている。VirtualBox用の仮想ハードディスクイメージのダウンロードのページ（http://www.ubuntulinux.jp/download/ja-remix-vhd） から

    　　ubuntu-ja-10.04.3-desktop-i386-vhd.zip　

    をダウンロードする（ubuntu-ja-12.04-desktop-i386-vhd.zipではFDR起動に失敗する可能性あり）。後は、このダウンロードのページに従ってインストールする。


[補足事項]

ホスト側のWindowsとゲスト側のLinuxの間でファイルを共有する方法
  1. VirtualBox Guest Additions をインストールする：
    (1) 仮想マシンを起動中にメニューの[デバイス(D)]から[Guest Additions のインストール]を選択する
    (2) "オートランの問合せを開く"を選択して[OK]→[実行する]

  2. Windows側の適当な場所に共有フォルダを作成する。

    　例： \C:\virtualbox\share

  3. VirtualBoxの「設定」の「共有フォルダ」に上記の1で作成したフォルダを追加する。

    　例：　フォルダのパス：　\C:\virtualbox\share
    　例：　フォルダ名：　share

  4. VirtualBoxでUbuntuを起動し、適当なディレクトリを作成して、上記の2で設定したフォルダにマウントする。

    　例：　sudo mkdir /media/vboxshare
    　例：　sudo mount.vboxsf share /media/vboxshare

  5. 以上により、Windowsの　\C:\virtualbox\share　と　Ubuntuの　\C:\virtualbox \share　を通してファイル交換できるようになる。



参考資料

CSP研究会の発表スライド（CSP研究会は年に3〜4回開催されている）。


2017/06/05 更新