SPINモデル検査―検証モデリング技法

SPINモデル検査―検証モデリング技法
中島 震



堅固なソフトウェアを作るにはどういうアプローチがとれるのだろうか。デザイン、プログラムの《正しさ》を検証するにはどうすればよいのだろうか。

SPINは、オートマトン、時相論理、グラフ•アルゴリズムの基礎技術から成り立っているそうです。

参考
SPINモデルチェッカ - Wikipedia