自動かき氷機の形式検証の話

夏なので自動かき氷機の「正しさ」を数学的に検証する話を書きます。 (この記事は以下のツイートから始まるスレッドの内容をまとめ直したものです。)

とりあえずかき氷機の抽象的な動作を記述したオートマトンを書きます。

このオートマトンだとボールを置かずにボタンを押したときに虚空に向かってかき氷を作るので、ボールがあるかどうかを検知するようにします。

これでもまだ動作中にボールを除いたときに虚空に向かってかき氷を作るので、そういうときは止まるようにします。

さて、モデル検査ツールであるNuSMVの形式でモデルを書いてみます。

動作中はボールがない (LTL で"G(state = running -> bowl)")という仕様を検証してみようとすると、反例が見つかります。ボタンを押す前にボールを取り除いた場合でも、そのままかき氷を作る仕様になっていました。

ということで、一度ボールが置かれた待機状態でボールが取り除かれた場合は初期状態に戻るようにしてみます。

このモデルでもまだエラーが出ます。このモデルだとボタンを押した直後にボールを取り除くと、初期状態に戻るまでの 1 ステップは虚空にボールをかき氷をばらまくようです。

頑張ればなんとかなるかもしれないですが、 そろそろお昼ご飯を食べたいので 今回は仕様の方を妥協して、「ボールがないなら次のステップでは動作していない」という仕様 (LTL 式だと G(!bowl -> X(state != running)))を検証してみます。できました。よかったよかった。