著者

グレーバー デヴィッド ワイズマン スージー 芳賀 達彦 森田 和樹 酒井 隆史

出版者

青土社

雑誌

現代思想

巻号頁・発行日

vol.46, no.17, pp.112-128, 2018-11

著者

森田 和樹

出版者

Waseda University

巻号頁・発行日

2005-02-02

---

有限状態遷移系に対する形式的手法,特にモデル検査手法を適用して,システムの仕様に対する妥当性を検証する方法は、近年、大きな成功をおさめている.限定モデル検査手法とは,モデル検査を論理式の充足可能性判定問題へと帰着して実現するものであり,初期状態から指定された回数の遷移のみを考慮して検証を行う.本研究では,限定モデル検査手法において検証時間の大部分を占める充足可能性の判定に焦点をあて,MPIライブラリを用いて並列化することにより高速な検査検証を実現した.性能は、我々の研究環境であるFOLON-IVを用いて測定を行った.実験では,指定された回数の遷移内でシステムが仕様を満たすことを示すのに最大60%の性能向上を達成した.また,遷移回数10〜30程度の問題でバグの発見に要する検証時間を大幅に短縮することができた.