自動かき氷機の形式検証の話
夏なので自動かき氷機の「正しさ」を数学的に検証する話を書きます。 (この記事は以下のツイートから始まるスレッドの内容をまとめ直したものです。)
自動かき氷機の形式検証をやりたい (そして実機で正しく動作することを確認するためにかき氷を作って食べたい)
— Masaki Waga (@MasWag) June 2, 2022
とりあえずかき氷機の抽象的な動作を記述したオートマトンを書きます。
このオートマトンだとボールを置かずにボタンを押したときに虚空に向かってかき氷を作るので、ボールがあるかどうかを検知するようにします。
これでもまだ動作中にボールを除いたときに虚空に向かってかき氷を作るので、そういうときは止まるようにします。
さて、モデル検査ツールであるNuSMVの形式でモデルを書いてみます。
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| MODULE main | |
| VAR | |
| bowl : boolean; | |
| button : boolean; | |
| state : {initial, wait, running, done}; | |
| ASSIGN | |
| init(bowl) := {FALSE, TRUE}; | |
| init(button) := {FALSE, TRUE}; | |
| init(state) := {initial}; | |
| next(bowl) := {FALSE, TRUE}; | |
| next(button) := {FALSE, TRUE}; | |
| next(state) := | |
| case | |
| state = initial & bowl : wait; | |
| state = wait & button : running; | |
| state = running & !bowl : initial; | |
| state = running : done; | |
| state = done & !bowl : initial; | |
| TRUE : state; | |
| esac; |
動作中はボールがない (LTL で"G(state = running -> bowl)")という仕様を検証してみようとすると、反例が見つかります。ボタンを押す前にボールを取り除いた場合でも、そのままかき氷を作る仕様になっていました。
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| *** This is NuSMV 2.6.0 (compiled on Sat Oct 20 18:58:24 2018) | |
| *** Enabled addons are: compass | |
| *** For more information on NuSMV see <http://nusmv.fbk.eu> | |
| *** or email to <nusmv-users@list.fbk.eu>. | |
| *** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>> | |
| *** Copyright (c) 2010-2014, Fondazione Bruno Kessler | |
| *** This version of NuSMV is linked to the CUDD library version 2.4.1 | |
| *** Copyright (c) 1995-2004, Regents of the University of Colorado | |
| *** This version of NuSMV is linked to the MiniSat SAT solver. | |
| *** See http://minisat.se/MiniSat.html | |
| *** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson | |
| *** Copyright (c) 2007-2010, Niklas Sorensson | |
| -- specification G (state = running -> bowl) is false | |
| -- as demonstrated by the following execution sequence | |
| Trace Description: LTL Counterexample | |
| Trace Type: Counterexample | |
| -> State: 1.1 <- | |
| bowl = FALSE | |
| button = FALSE | |
| state = initial | |
| -> State: 1.2 <- | |
| bowl = TRUE | |
| -> State: 1.3 <- | |
| bowl = FALSE | |
| button = TRUE | |
| state = wait | |
| -> State: 1.4 <- | |
| button = FALSE | |
| state = running | |
| -- Loop starts here | |
| -> State: 1.5 <- | |
| state = initial | |
| -> State: 1.6 <- |
ということで、一度ボールが置かれた待機状態でボールが取り除かれた場合は初期状態に戻るようにしてみます。
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| MODULE main | |
| VAR | |
| bowl : boolean; | |
| button : boolean; | |
| state : {initial, wait, running, done}; | |
| ASSIGN | |
| init(bowl) := {FALSE, TRUE}; | |
| init(button) := {FALSE, TRUE}; | |
| init(state) := {initial}; | |
| next(bowl) := {FALSE, TRUE}; | |
| next(button) := {FALSE, TRUE}; | |
| next(state) := | |
| case | |
| state = initial & bowl : wait; | |
| state = wait & !bowl : initial; | |
| state = wait & button & bowl: running; | |
| state = running & !bowl : initial; | |
| state = running : done; | |
| state = done & !bowl : initial; | |
| TRUE : state; | |
| esac; | |
| LTLSPEC G(state = running -> bowl) |
このモデルでもまだエラーが出ます。このモデルだとボタンを押した直後にボールを取り除くと、初期状態に戻るまでの 1 ステップは虚空にボールをかき氷をばらまくようです。
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| *** This is NuSMV 2.6.0 (compiled on Sat Oct 20 18:58:24 2018) | |
| *** Enabled addons are: compass | |
| *** For more information on NuSMV see <http://nusmv.fbk.eu> | |
| *** or email to <nusmv-users@list.fbk.eu>. | |
| *** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>> | |
| *** Copyright (c) 2010-2014, Fondazione Bruno Kessler | |
| *** This version of NuSMV is linked to the CUDD library version 2.4.1 | |
| *** Copyright (c) 1995-2004, Regents of the University of Colorado | |
| *** This version of NuSMV is linked to the MiniSat SAT solver. | |
| *** See http://minisat.se/MiniSat.html | |
| *** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson | |
| *** Copyright (c) 2007-2010, Niklas Sorensson | |
| -- specification G (state = running -> bowl) is false | |
| -- as demonstrated by the following execution sequence | |
| Trace Description: LTL Counterexample | |
| Trace Type: Counterexample | |
| -> State: 1.1 <- | |
| bowl = FALSE | |
| button = FALSE | |
| state = initial | |
| -> State: 1.2 <- | |
| bowl = TRUE | |
| -> State: 1.3 <- | |
| button = TRUE | |
| state = wait | |
| -> State: 1.4 <- | |
| bowl = FALSE | |
| button = FALSE | |
| state = running | |
| -- Loop starts here | |
| -> State: 1.5 <- | |
| state = initial | |
| -> State: 1.6 <- |
頑張ればなんとかなるかもしれないですが、 そろそろお昼ご飯を食べたいので 今回は仕様の方を妥協して、「ボールがないなら次のステップでは動作していない」という仕様 (LTL 式だと G(!bowl -> X(state != running)))を検証してみます。できました。よかったよかった。
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| MODULE main | |
| VAR | |
| bowl : boolean; | |
| button : boolean; | |
| state : {initial, wait, running, done}; | |
| ASSIGN | |
| init(bowl) := {FALSE, TRUE}; | |
| init(button) := {FALSE, TRUE}; | |
| init(state) := {initial}; | |
| next(bowl) := {FALSE, TRUE}; | |
| next(button) := {FALSE, TRUE}; | |
| next(state) := | |
| case | |
| state = initial & bowl : wait; | |
| state = wait & !bowl : initial; | |
| state = wait & button & bowl: running; | |
| state = running & !bowl : initial; | |
| state = running : done; | |
| state = done & !bowl : initial; | |
| TRUE : state; | |
| esac; | |
| LTLSPEC G(!bowl -> X(state != running) ) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| *** This is NuSMV 2.6.0 (compiled on Sat Oct 20 18:58:24 2018) | |
| *** Enabled addons are: compass | |
| *** For more information on NuSMV see <http://nusmv.fbk.eu> | |
| *** or email to <nusmv-users@list.fbk.eu>. | |
| *** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>> | |
| *** Copyright (c) 2010-2014, Fondazione Bruno Kessler | |
| *** This version of NuSMV is linked to the CUDD library version 2.4.1 | |
| *** Copyright (c) 1995-2004, Regents of the University of Colorado | |
| *** This version of NuSMV is linked to the MiniSat SAT solver. | |
| *** See http://minisat.se/MiniSat.html | |
| *** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson | |
| *** Copyright (c) 2007-2010, Niklas Sorensson | |
| -- specification G (!bowl -> X state != running) is true |