SPIN是用於形式化驗證並發程序的模型檢測工具。Promela是SPIN的輸入語法，通過LTL(Linear Temporal Logic)或者斷言來對驗證屬性進行規約，並給出違反驗證屬性情況下的反例路徑
github下載SPIN包
linux SPIN 安裝(官方編譯版本)
unzip ~/Spin-master.zip -d ~/spin-master # 本文Spin-master.zip位於家目錄
cd ~/spin-master/Bin
gunzip spin651_linux64.gz # 選擇一個linux版本解壓
chmod +x spin651_linux64
sudo cp spin651_linux64 /usr/local/bin/spin
spin -V
linux SPIN 安裝(自己編譯)用官方已經編譯好的SPIN，有時候回出現問題，則需要自己編譯。
unzip ~/Spin-master.zip -d ~/spin-master # 本文Spin-master.zip位於家目錄
cd ~/spin-master/Src
sudo apt-get install byacc #安裝byacc
sudo apt-get install gcc #安裝gcc
make #編譯后出現spin文件
sudo cp ./spin /usr/local/bin/spin
spin -V
linux ISPIN(linux的SPIN圖形化工具) 安裝
cd ~/spin-master/optional_gui
sudo apt-get isntall tk # 安裝依賴
chmod +x ./ispin.tcl
sudo cp ispin.tcl /usr/local/bin/ispin
ispin # 打開ispn
java JSPIN
JSPIN https://github.com/motib/jspin
其他安裝參考http://spinroot.com/spin/Man/README.html
SPIN 學習參考資料
Promela 語法
SPIN 命令行參數介紹
pan 命令行參數介紹
spin 基本算法原理 SpinIntro.pdf
SPIN推薦書籍
Principles of the Spin Model Checker（包含模型檢測知識、Promela語法、LTL公式）
