LoginSignup
19
9

More than 3 years have passed since last update.

@shinsa82(Shin Saito)

NuSMVによるモデル検査入門 (1) ステートマシンを定義する

Last updated at Posted at 2018-02-16

この前書いた記事はあまりにもやっつけだったので整理してみる。

概要

この記事は、シンボリックモデルチェッカNuSMV (http://nusmv.fbk.eu/) を使って、モデル検査を行うチュートリアルである。

NuSMVのバージョンはv2.6.0とする。バージョンによって機能がobsoleteされたり変更されたりするので、古いバージョン用の資料を読むときには注意されたい。

基礎知識

知ってるならスキップしてください。

モデル検査 (Model Checking) とは

状態遷移系が論理式を満たすかどうかを検査すること。

より正確には、あるKripke構造がある時相論理式を満たすか否かを検査することである。
一般に数理論理学で、データ構造 $M$ が論理式 $\phi$ を成り立たせる場合に $M\models\phi$ と書き「$M$ は $\phi$ のモデルである」と呼ぶことから、この検査をモデル検査と呼ぶ。

例えば、並列プログラムの検証に用いることができ、安全性 (safety):

  • 2つのスレッドが同時にクリティカルセクションに入らないこと

ならびに活性 (liveness):

  • ハンドシェイクプロトコルが必ず終了すること
  • プログラムがデッドロックに陥らないこと

といった性質を記述・検証するために使われる。

時相論理 (Temporal Logic) とは

状態遷移系の性質を記述できる論理。

対象とする系 (Kripke構造) の状態は移り変わっていく。その遷移の各時点および遷移列に対しての性質を記述できる論理を時相論理と呼ぶ。様相論理 (Modal Logic) の一種である。

  • 「どの状態においてもPが成り立つ」を表す []P (もしくは G(P))
  • 「いずれPが成り立つ」を表す <>P (もしくは F(P))
  • 「すべての遷移列に対してQが成り立つ」を意味する A(Q)
  • 「ある遷移列が存在してQが成り立つ」を意味する E(Q)

などの演算子が古典論理に追加されている。

著名な記法として LTL (Linear Temporal Logic; 線形論理) や CTL (Computational Tree Logic; 計算木論理) がある。これらはいずれもより強力な CTL* のサブセットである。NuSMVではLTLおよびCTLで書いた式の検査が行える。

モデルチェッカ/モデル検査器 (Model Checker) とは

モデル検査を自動で行ってくれるツール。

一般的なモデル検査器は、モデルが与えられた論理式を満たす場合には満たすことを表示し、満たさない場合には反例 (counterexample) を表示する。

著名なモデル検査器として、SPIN (スピン) は覚えておくとよい。

シンボリック (Symbolic) モデルチェッカ とは

状態を論理式として表現することにより、効率と検査可能性を向上したタイプのモデル検査器。

基本的なモデル検査器は初期状態から到達可能な状態を順次探索して1つずつ記憶領域に格納していくため、状態爆発との闘いになるし、無限状態を扱えない。
そうではなく、状態の集合の表現として、それらが満たす論理式を採用し、論理式の操作として検査を行うことにより、莫大もしくは無限の状態数を持つ系に対しての検査を可能にしたのがKen McMillanらの提案したシンボリックモデル検査である。これらの検査器はBDD (binary decision diagram) と呼ばれるデータ構造を用いたり、SAT (命題論理の充足性判定) ソルバーを利用している。以前は数百万状態がモデル検査器で扱える限界であったが、10^20程度の状態を扱えるようになった。NuSMVはシンボリックなモデル検査器である。

NuSMV の学習用リソース (チュートリアル・ドキュメント)

まずは公式を読むのがおすすめ (英語)。どちらもあまり親切ではないが、バージョンアップに細かに追随しているのは好感が持てる。

最近見つけたこれがわかりやすい (英語)。

NuSMVのセットアップ

  • http://nusmv.fbk.eu/ からNuSMVをインストールする。商用でなければZCHAFF付属版でいいと思われる。
  • bin/nusmv にパスを通す。

実行してこんな感じのメッセージが出ればOK。

~/nusmv-tutorial$ nusmv
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:31:33 2015)
*** 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

WARNING *** This version of NuSMV is linked to the zchaff SAT         ***
WARNING *** solver (see http://www.princeton.edu/~chaff/zchaff.html). ***
WARNING *** Zchaff is used in Bounded Model Checking when the         ***
WARNING *** system variable "sat_solver" is set to "zchaff".          ***
WARNING *** Notice that zchaff is for non-commercial purposes only.   ***
WARNING *** NO COMMERCIAL USE OF ZCHAFF IS ALLOWED WITHOUT WRITTEN    ***
WARNING *** PERMISSION FROM PRINCETON UNIVERSITY.                     ***
WARNING *** Please contact Sharad Malik (malik@ee.princeton.edu)      ***
WARNING *** for details.                                              ***

Input file is (null). You must set the input file before.

Aborting batch mode

NuSMV terminated by a signal

Aborting batch mode

NuSMVでシンプルなステートマシンを定義する

目標は並列システムを記述することだが、まずはシンプルな状態遷移系を書いてみる。
次のリストはカウンタxの値を増やしていくものである。ただしx=10になると増やすのをやめる。
これは何か仕事をしていると思ってもらうとよい。x=10が仕事の完了に相当する。

ex01.smv
MODULE main
    VAR
        x: 0..10;
    ASSIGN
        init(x) := 0;
        next(x) := x=10 ? 10 : x+1;

行末のセミコロンを忘れないように。なお等号判定が=であり、代入が:=であるので注意。
また、NuSMVは複数のモジュールを利用した記述が可能であるが、mainモジュールがメインルーチンとなるので必ず定義すること。

MODULEセクション

モジュールを定義することができる。モジュールを連結して複雑なプロセスからなるシステムを記述できる。
MODULE foo(in, out) のように引数を設けることができ、モジュールのインスタンス化のときに、他のモジュール内の変数を指定することができる。

各モジュールは次で説明するように、VARセクションとASSIGNセクションを持つ。

VARセクション

状態変数とその型 (取りうる値) を定義するセクションである。ここではxの値域を0から10までの整数であると定義している。他にも集合{2,3,5,7}が書けたり、数字以外のシンボル値{green,yellow,red}が書けたりする。シンボルを使う場合は予約語とかぶらないように注意すること。

ASSIGNセクション

状態遷移を定義するセクションである。init()で初期値、next()で遷移先の状態を定義する。
ここではxの遷移先はC言語的な3項演算子で記述している。case文も使える。
非決定的な代入もできることに留意されたい。例えばinit(x) := {0,1};とすると0か1が非決定的に初期値となる。

遷移系の他の記述方法もあるが、自分も試したことがないので省略する。

NuSMVを動かしてみる

バッチモード: 論理式をモデル検査で検証する

nusmv <ファイル名>で実行するとバッチモードになる。ファイルを読み込んで検査条件を検査し、結果を表示する。
では、さきほどのファイルを実行してみる。今はまだ検査条件を記述していないので何も表示されずに終わる。

~/nusmv-tutorial/chap01$ nusmv ex01.smv 
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:31:33 2015)
*** 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

WARNING *** This version of NuSMV is linked to the zchaff SAT         ***
WARNING *** solver (see http://www.princeton.edu/~chaff/zchaff.html). ***
WARNING *** Zchaff is used in Bounded Model Checking when the         ***
WARNING *** system variable "sat_solver" is set to "zchaff".          ***
WARNING *** Notice that zchaff is for non-commercial purposes only.   ***
WARNING *** NO COMMERCIAL USE OF ZCHAFF IS ALLOWED WITHOUT WRITTEN    ***
WARNING *** PERMISSION FROM PRINCETON UNIVERSITY.                     ***
WARNING *** Please contact Sharad Malik (malik@ee.princeton.edu)      ***
WARNING *** for details.                                              ***

もし文法エラーがある場合はその旨が表示されてabortする。

~/nusmv-tutorial/chap01$ nusmv ex01_bad.smv 
(略)
WARNING *** Please contact Sharad Malik (malik@ee.princeton.edu)      ***
WARNING *** for details.                                              ***


file ex01_bad.smv: line 6: at token "next": syntax error


file ex01_bad.smv: line 6: Parser error

NuSMV terminated by a signal

Aborting batch mode

検査条件の定義

検査条件はLTLSPECまたはCTLSPECセクションに記述する。
今回はxの値がいつか必ず10になることを検査条件としてみる。ファイルの末尾に以下を追記したファイルをex02.smvとする。

ex02.smv(一部)
    LTLSPEC F (x=10);

FはFinallyで、遷移パスのどこかにx=10となる状態があることを意味している。
実行すると、検査条件が真であることが表示される。
なお、LTLの式は先頭にAを付けたCTLの式であるかのように検査される。今回の例では、「初期状態からありえるすべての遷移パスにおいて、どこかにx=10となる状態があること」と解釈される。

~/nusmv-tutorial/chap01$ nusmv ex02.smv
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:31:33 2015)
*** 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

WARNING *** This version of NuSMV is linked to the zchaff SAT         ***
WARNING *** solver (see http://www.princeton.edu/~chaff/zchaff.html). ***
WARNING *** Zchaff is used in Bounded Model Checking when the         ***
WARNING *** system variable "sat_solver" is set to "zchaff".          ***
WARNING *** Notice that zchaff is for non-commercial purposes only.   ***
WARNING *** NO COMMERCIAL USE OF ZCHAFF IS ALLOWED WITHOUT WRITTEN    ***
WARNING *** PERMISSION FROM PRINCETON UNIVERSITY.                     ***
WARNING *** Please contact Sharad Malik (malik@ee.princeton.edu)      ***
WARNING *** for details.                                              ***

-- specification  F x = 10  is true

では、成り立たない条件を書くとどうなるだろうか。
先ほどの条件の代わりに、「常にx=10である」という次の条件を指定したものをex03.smvとする。

ex03.smv(一部)
    LTLSPEC G (x=10);

GはGloballyのことで、パス上のすべての状態で性質が成り立つことを要求する。
これを実行すると条件が偽であることと、反例が1つ表示される。

~/nusmv-tutorial/chap01$ nusmv ex03.smv
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:31:33 2015)

(略)

-- specification  G x = 10  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    x = 0
  -> State: 1.2 <-
    x = 1
  -> State: 1.3 <-
    x = 2
  -> State: 1.4 <-
    x = 3
  -> State: 1.5 <-
    x = 4
  -> State: 1.6 <-
    x = 5
  -> State: 1.7 <-
    x = 6
  -> State: 1.8 <-
    x = 7
  -> State: 1.9 <-
    x = 8
  -> State: 1.10 <-
    x = 9
  -- Loop starts here
  -> State: 1.11 <-
    x = 10
  -> State: 1.12 <-

今回定義した遷移系では可能なパスは上記の1つしかないので、それが表示されている。
筆者も自信がないが、-- Loop starts here以下のState1.11および1.12部分がループしているような無限のパスを表示していると思われる。このパスは変更のあった変数だけが表示されている。よって1.12でのxの値は1.11と等しい10である。
なお、一般には時相論理が扱うパスは無限長であるのでこのような反例が表示されることに注意されたい。

対話モード (シミュレーション)

NuSMVには遷移系をステップ実行する対話モードがある。説明しようかと思ったが眠いので次回に譲ることにする。
対話モードで起動するにはnusmv -int <ファイル名>とするとよい。

19
9
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
19
9