How to install free softwares in Linux

last update: 29 Sep 2004

プロトコル検証用言語Promelaは1980年代後半にAT&Tベル研究所のDr. G.J.Holzmmanによって開発され、 シミュレータ"spin"は今でも引続き機能拡張と改良が続けれています。

"xspin"というTcl/TkベースのGUIプログラムを介して"spin"を実行することができます。

開発当初の目的は"通信プロトコルの検証"だったのですが、 時代の流れを受けてか、ここ2年くらいの間に"分散システムのソフトウエアの検証"に変わってきました。
最近の雑誌記事によれば、デニス・リッチーがインタビューに答えて、 Dr. G.J.Holzmmanが共同研究を行なっていると語っており、 spinとPlain9(デニス・リッチーが開発しているOS)の連係にも興味がもたれます。

5.2 ソフトの入手

以下のURLから最新の"spin"をダウンロードできます。現在の最新バージョンは3.4.7です(2001年4月現在)。

ftp://netlib.bell-labs.com/netlib/spin/

注意：	spinのコンパイルには"yacc"が必要です。 xspinの実行にはwish4.2以上のTcl/Tk処理系が必要です。

spinのアーカイブは作業を行なっているディレクトリにファイルを展開してしまうので、 予めspin用のディレクトリを作っておきます。 ここでは新たにディレクトリ$Work/spinを作り、ファイルを展開します。
作業ディレクトリ$Workは任意のディレクトリです。

% cd $Work
% mkdir spin
% cd ./spin
% gzip -cd spin347.tar.gz | tar xvf -

5.3.1 spinのインストール

ディレクトリ$Work/spin/Src3.4に移動し、"make"を実行します。
% cd Src3.4
% make


makeが終了すると実行ファイル"spin"ができますので、適当なディレクトリにコピーして下さい。 ここではディレクトリ/usr/local/binにコピーします。

% cp spin /usr/local/bin




5.3.2 xspinのインストール

ディレクトリ$Work/spin/XSrc3.4に移動します。
% cd $work/spin/XSrc3.4


ディレクトリ$Work/spin/XSrc3.4以下の"xspin347.tcl"を、 各自の環境にあわせて変更します。

• wish
  先頭にあるwishのパスを各自の環境にあわせて変更して下さい。デフォルトでは"/usr/local/bin/wish" となっています。
• set SPIN
  "spin"の実行ファイルを指定します。なるべくなら絶対パスで指定した方がよいでしょう。 今回の例では以下のようになります。
  

  set SPIN "/usr/local/bin/spin"

  
  
• CC
  デフォルトではgccを使います。

変更が終った"xspin347.tcl"をパスの通ったディレクトリにコピーします。 例えば：

% cp ./xspin347.tcl /usr/local/bin/xspin

注意：	本が出版されたのは1991年(日本語版は1994年)で、説明が古い部分があります。 例えば： "ラベル付けされた状態の条件文(日本語版171ページ)"は、本では":"を使っていますが、 現在のバージョンでは"@"を使います。

5.5.1 オリジナルサイト

"spin"のオリジナルサイトは以下の通りです：


http://netlib.bell-labs.com/netlib/spin/index.html




5.5.2 参考文献

開発者による本があります。
・ Prentice Hall, "Design and Validation of Computer Protocols" by G.J. Holzmman
・日本語版：カットシステム "コンピュータプロトコルの設計法"


また、上記の原本のPS版、PDF版がオリジナルサイトからオンラインで入手できます。

home |index |previous |next |contents

since 04/Oct/2004