抽象状態機械の到達性解析による安全性の簡易検証

本論文では、抽象状態機械の到達性解析による並列プロセスの安全性検証について述べる。安全性は、「悪い状態に到達しない」という到達性を解析することで検証可能であり、また、モデルの大きさは同様な状態を同一視することで低く抑えられることが期待できる。実証実験として、排他制御アルゴリズムであるピーターソンのアルゴリズムを検証するためのシンプルなアルゴリズムと、その実装を行った。その結果、ピーターソンのアルゴリズム程度のプロセスの検証であれば、普通のノート PC であっても 0.05 秒未満で解析が終了することがわかった。

千葉商大紀要