SPIN
SPIN(Simple Promela INterpreter)
Promela でモデル化されたシステムを検証
Promela (PROcess MEta LAnguage)
プロセスの振る舞いを記述する DSL
手続き指向、C 言語風文法
非同期分散アルゴリズムを非決定的オートマトンとしてモデル化する
オートマトンに基づく模型検査器(model checker)
モデル検査
線形時相論理 (LTL)
OSS
マルチスレッドのモデル記述言語
マルチプロセスのものにも良さそう?
公式: Spin - Formal Verification
SPINのインストール
Spin - Version 6.4 - December 2018
macOS、Linuxはここを参考してインストールするとよさそう
SPINインストール手順 - Qiita
下記は公式のインストール手順
Spin - Version 6.4 - December 2018
code:memo
$ make
yacc -v -d spin.y
make: yacc: No such file or directory
make: *** makefile:46: spin.o Error 127
sudo apt install yaccをしたらbyaccなるものがインストールされたけどそのあとのコンパイルが通ったので大丈夫なのだと思う
code:memo
$ sudo apt install yacc
sudo password for pogin503:
Reading package lists... Done
Building dependency tree... Done
Reading state information... Done
Note, selecting 'byacc' instead of 'yacc'
The following NEW packages will be installed:
byacc
0 upgraded, 1 newly installed, 0 to remove and 114 not upgraded.
Need to get 86.2 kB of archives.
After this operation, 217 kB of additional disk space will be used.
Get:1 http://archive.ubuntu.com/ubuntu jammy/universe amd64 byacc amd64 1:2.0.20220114-1 86.2 kB
Fetched 86.2 kB in 1s (64.7 kB/s)
Selecting previously unselected package byacc.
(Reading database ... 52558 files and directories currently installed.)
Preparing to unpack .../byacc_1%3a2.0.20220114-1_amd64.deb ...
Unpacking byacc (1:2.0.20220114-1) ...
Setting up byacc (1:2.0.20220114-1) ...
update-alternatives: using /usr/bin/byacc to provide /usr/bin/yacc (yacc) in auto mode
Processing triggers for man-db (2.10.2-1) ...
code:memo
$ type spin
-bash: type: spin: not found
make installで配置はないようなので、できたファイルをコピーする
$ cp -i spin /usr/local/bin
資料
本
Amazon.co.jp: SPIN モデル検査: 検証モデリング技法 : 中島 震: 本
SPINによる設計モデル検証―モデル検査の実践ソフトウェア検証 (トップエスイー実践講座)
公式: Spin - Formal Verification
Spin - Formal Verification - Books
猫でもわかる! モデル検査器 SPIN 入門
SPINモデルチェッカ - Wikipedia
#TODO_2
#形式手法