AUTOSAR CountdownAdvent Calendar 2022

@kaizen_nagoya(Dr. Kiyoshi Ogawa)

NuSMV入門４日で学ぶモデル検査初級編

Last updated at 2025-04-25Posted at 2018-03-18

４日で学ぶモデル検査　初級編

https://www.amazon.co.jp/dp/4860431197/

モデル検査初級編―基礎から実践まで4日で学べる (CVS教程)
https://www.amazon.co.jp/dp/4764955059/

NuSMVとSPINで記述している。

導入

導入
http://nusmv.fbk.eu/

Getting the NuSMV Source Code
http://nusmv.fbk.eu/NuSMV/download/getting_src-v2.html

Getting the NuSMV Binary Code
http://nusmv.fbk.eu/NuSMV/download/getting_bin-v2.html

５種類あります。
GNU/Linux libc6 (686) 32-bit
GNU/Linux libc6 (x86) 64-bit
MacOSX Darwin (x86) 64-bit
Windows archive 32-bit (586)
Windows archive 64-bit (x86)

With ZCHAFFとwithout ZCHAFFが選べます。

 ZCHAFF is for non-commercial purposes only. 
NO COMMERCIAL USE OF ZCHAFF IS ALLOWED WITHOUT WRITTEN PERMISSION FROM PRINCETON UNIVERSITY. 
Please contact Sharad Malik (malik@ee.princeton.edu) for details. |

sample

systemalpha.smv

MODULE main

VAR
a:{0,1,2};
b:{0,1,2};
sw:{on, off};

ASSIGN
 init(a) := 0;
 next(a) := case
    b = 1:a;
    1:(a+1) mod 3;
    esac;

init(b) := 0;
next(b) := case
    a = b:b;
    1 :(b+1) mod 3;

init(sw) : = off;
    a=2 & b = 2: on;
    a=1 & b = 1: off;
    1 :sw;
    esac;

LTLSPEC G ( sw = off -> F (sw = on))
LTLSPEC G ( sw = on -> F (sw = off))

実行結果

$ ./NuSMV systemalpha.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.                                              ***


file systemalpha.smv: line 20: at token "init": syntax error


file systemalpha.smv: line 20: Parser error

NuSMV terminated by a signal

Aborting batch mode

systemalpha.smv

MODULE main

VAR
a:{0,1,2};
b:{0,1,2};
sw:{on, off};

ASSIGN
 init(a) := 0;
 next(a) := case
    b = 1:a;
    1:(a+1) mod 3;
    esac;

init(b) := 0;
next(b) := case
    a = b:b;
    1 :(b+1) mod 3;
    esac;

init(sw) : = off;
    a=2 & b = 2: on;
    a=1 & b = 1: off;
    1 :sw;
    esac;

LTLSPEC G ( sw = off -> F (sw = on))
LTLSPEC G ( sw = on -> F (sw = off))

bash

file systemalpha.smv: line 21: at token ":": syntax error

file systemalpha.smv: line 21: Parser error

NuSMV terminated by a signal

Aborting batch mode

teisei

init(sw) := off;

空白を詰めた。

bash

file systemalpha.smv: line 22: at token "=": syntax error
file systemalpha.smv: line 22: Parser error

NuSMV terminated by a signal

Aborting batch mode

tsuika

next(sw) := case

追加

bash

TYPE ERROR file systemalpha.smv: line 12 : illegal left operand type of ":". It should be boolean, but is integer

TYPE ERROR file systemalpha.smv: line 18 : illegal left operand type of ":". It should be boolean, but is integer

TYPE ERROR file systemalpha.smv: line 25 : illegal left operand type of ":". It should be boolean, but is integer

file systemalpha.smv: Type System Violation detected


Aborting batch mode

NuSMV terminated by a signal

Aborting batch mode

実行

bash

TYPE ERROR file systemalpha.smv: line 12 : illegal left operand type of ":". It should be boolean, but is integer

TYPE ERROR file systemalpha.smv: line 18 : illegal left operand type of ":". It should be boolean, but is integer

TYPE ERROR file systemalpha.smv: line 25 : illegal left operand type of ":". It should be boolean, but is integer

file systemalpha.smv: Type System Violation detected

Aborting batch mode

NuSMV terminated by a signal

Aborting batch mode

Qiita on NuSMV

NuSMVでコンセンサスアルゴリズム (の超一部) をモデル検査する
https://qiita.com/shinsa82/items/c66b91047c2174929ae1

NuSMVによるモデル検査入門 (1) ステートマシンを定義する
https://qiita.com/shinsa82/items/cd4d95c616bf1da852ce

参考文献

モデル検査ツールについて
Copyright© FormalTech Co., Ltd. all rights reserved.
株式会社フォーマルテック
http://www.formaltech.co.jp/aboutMCtool.pdf

NuSMV を用いた CTL*のモデル検査器の実装
東京工業大学理学部情報科学科藤原一貴(0521236)
平成 20 年度卒業論文
指導教官佐々政孝教授 2009年2月5日
http://www.is.titech.ac.jp/~sassa/lab/papers-written/05B21236-fujiwara.pdf

モデル検査ツール NuSMV を用いたオントロジー検証 Ontology Verification using the Model Checker NuSMV, 阿部雄貴
http://oberon.nagaokaut.ac.jp/katsuk/papers/fit/11/data/pdf/B-005.pdf

NuSMVによるモデリング.
http://lis2.huie.hokudai.ac.jp/~kurihara/classes/Program/nusmvspin.ppt

＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
This article is an individual impression based on the individual's experience. It has nothing to do with the organization or business to which I currently belong.

日本語（０）一欄
https://qiita.com/kaizen_nagoya/items/7498dcfa3a9ba7fd1e68

英語(0) 一覧
https://qiita.com/kaizen_nagoya/items/680e3f5cbf9430486c7d

音楽　一覧(0)
https://qiita.com/kaizen_nagoya/items/b6e5f42bbfe3bbe40f5d

「@kazuo_reve 新人の方によく展開している有益な情報」確認一覧
https://qiita.com/kaizen_nagoya/items/b9380888d1e5a042646b

鉄道（０）鉄道のシステム考察はてっちゃんがてつだってくれる
https://qiita.com/kaizen_nagoya/items/faa4ea03d91d901a618a

OSEK OS設計の基礎　OSEK(100)
https://qiita.com/kaizen_nagoya/items/7528a22a14242d2d58a3

coding (101) 一覧を作成し始めた。omake:最近のQiitaで表示しない5つの事象
https://qiita.com/kaizen_nagoya/items/20667f09f19598aedb68

官公庁・学校・公的団体（NPOを含む）システムの課題、官（０）
https://qiita.com/kaizen_nagoya/items/04ee6eaf7ec13d3af4c3

「はじめての」シリーズ　ベクタージャパン　
https://qiita.com/kaizen_nagoya/items/2e41634f6e21a3cf74eb

AUTOSAR(0)Qiita記事一覧, OSEK(75)
https://qiita.com/kaizen_nagoya/items/89c07961b59a8754c869

プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945

LaTeX(0) 一覧　
https://qiita.com/kaizen_nagoya/items/e3f7dafacab58c499792

自動制御、制御工学一覧（０）
https://qiita.com/kaizen_nagoya/items/7767a4e19a6ae1479e6b

Rust(0) 一覧　
https://qiita.com/kaizen_nagoya/items/5e8bb080ba6ca0281927

programの本質は計画だ。programは設計だ。
https://qiita.com/kaizen_nagoya/items/c8545a769c246a458c27

登壇直後版色使い(JIS安全色) Qiita Engineer Festa 2023〜私しか得しないニッチな技術でLT〜スライド編 0.15
https://qiita.com/kaizen_nagoya/items/f0d3070d839f4f735b2b

プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945

逆も真：社会人が最初に確かめるとよいこと。OSEK(69)、Ethernet(59)
https://qiita.com/kaizen_nagoya/items/39afe4a728a31b903ddc

統計の嘘。仮説（127）
https://qiita.com/kaizen_nagoya/items/63b48ecf258a3471c51b

自分の言葉だけで論理展開できるのが天才なら、文章の引用だけで論理展開できるのが秀才だ。仮説（136）
https://qiita.com/kaizen_nagoya/items/97cf07b9e24f860624dd

参考文献駆動執筆(references driven writing)・デンソークリエイト編
https://qiita.com/kaizen_nagoya/items/b27b3f58b8bf265a5cd1

「何を」よりも「誰を」。１０年後のために今見習いたい人たち
https://qiita.com/kaizen_nagoya/items/8045978b16eb49d572b2

Qiitaの記事に３段階または５段階で到達するための方法
https://qiita.com/kaizen_nagoya/items/6e9298296852325adc5e

出力(output)と呼ばないで。これは状態(state)です。
https://qiita.com/kaizen_nagoya/items/80b8b5913b2748867840

祝休日・謹賀新年 2025年の目標
https://qiita.com/kaizen_nagoya/items/dfa34827932f99c59bbc

Qiita 1年間をまとめた「振り返りページ」＠2024
https://qiita.com/kaizen_nagoya/items/ed6be239119c99b15828

2024 参加・主催Calendarと投稿記事一覧 Qiita(248)
https://qiita.com/kaizen_nagoya/items/d80b8fbac2496df7827f

主催Calendar2024分析 Qiita(254)
https://qiita.com/kaizen_nagoya/items/15807336d583076f70bc

Calendar 統計
https://qiita.com/kaizen_nagoya/items/e315558dcea8ee3fe43e

LLM 関連 Calendar 2024
https://qiita.com/kaizen_nagoya/items/c36033cf66862d5496fa

Large Language Model Related Calendar
https://qiita.com/kaizen_nagoya/items/3beb0bc3fb71e3ae6d66

博士論文 Calendar 2024 を開催します。
https://qiita.com/kaizen_nagoya/items/51601357efbcaf1057d0

博士論文(0)関連記事一覧
https://qiita.com/kaizen_nagoya/items/8f223a760e607b705e78

coding (101) 一覧を作成し始めた。omake:最近のQiitaで表示しない5つの事象
https://qiita.com/kaizen_nagoya/items/20667f09f19598aedb68

あなたは「勘違いまとめ」から、勘違いだと言っていることが勘違いだといくつ見つけられますか。人間の間違い(human error(125))の種類と対策
https://qiita.com/kaizen_nagoya/items/ae391b77fffb098b8fb4

プログラマの「プログラムが書ける」思い込みは強みだ。３つの理由。仮説（168）統計と確率(17) , OSEK(79)
https://qiita.com/kaizen_nagoya/items/bc5dd86e414de402ec29

出力(output)と呼ばないで。これは状態(state)です。
https://qiita.com/kaizen_nagoya/items/80b8b5913b2748867840

これからの情報伝達手段の在り方について考えてみよう。炎上と便乗。
https://qiita.com/kaizen_nagoya/items/71a09077ac195214f0db

ISO/IEC JTC1 SC7 Software and System Engineering
https://qiita.com/kaizen_nagoya/items/48b43f0f6976a078d907

アクセシビリティの知見を発信しよう！（再び）
https://qiita.com/kaizen_nagoya/items/03457eb9ee74105ee618

統計論及確率論輪講（再び）
https://qiita.com/kaizen_nagoya/items/590874ccfca988e85ea3

読者の心をグッと惹き寄せる7つの魔法
https://qiita.com/kaizen_nagoya/items/b1b5e89bd5c0a211d862

「@kazuo_reve 新人の方によく展開している有益な情報」確認一覧
https://qiita.com/kaizen_nagoya/items/b9380888d1e5a042646b

ソースコードで議論しよう。日本語で議論するの止めましょう（あるプログラミング技術の議論報告）
https://qiita.com/kaizen_nagoya/items/8b9811c80f3338c6c0b0

脳内コンパイラの3つの危険
https://qiita.com/kaizen_nagoya/items/7025cf2d7bd9f276e382

心理学の本を読むよりはコンパイラ書いた方がよくね。仮説（34）
https://qiita.com/kaizen_nagoya/items/fa715732cc148e48880e

NASAを超えるつもりがあれば読んでください。
https://qiita.com/kaizen_nagoya/items/e81669f9cb53109157f6

データサイエンティストの気づき!「勉強して仕事に役立てない人。大嫌い!!」『それ自分かも?』ってなった!!!
https://qiita.com/kaizen_nagoya/items/d85830d58d8dd7f71d07

「ぼくの好きな先生」「人がやらないことをやれ」プログラマになるまで。仮説（37）　
https://qiita.com/kaizen_nagoya/items/53e4bded9fe5f724b3c4

なぜ経済学徒を辞め、計算機屋になったか（経済学部入学前・入学後・卒業後対応）転職(1)
https://qiita.com/kaizen_nagoya/items/06335a1d24c099733f64

プログラミング言語教育のXYZ。仮説（52）
https://qiita.com/kaizen_nagoya/items/1950c5810fb5c0b07be4

【24卒向け】9ヶ月後に年収１０００万円を目指す。二つの関門と三つの道。
https://qiita.com/kaizen_nagoya/items/fb5bff147193f726ad25

「【25卒向け】Qiita Career Meetup for STUDENT」予習の勧め
https://qiita.com/kaizen_nagoya/items/00eadb8a6e738cb6336f

大学入試不合格でも筆記試験のない大学に入って卒業できる。卒業しなくても博士になれる。
https://qiita.com/kaizen_nagoya/items/74adec99f396d64b5fd5

全世界の不登校の子供たち「博士論文」を書こう。世界子供博士論文遠隔実践中心安全(99)
https://qiita.com/kaizen_nagoya/items/912d69032c012bcc84f2

日本のプログラマが世界で戦える16分野。仮説(53),統計と確率(25) 転職(32)、Ethernet(58)
https://qiita.com/kaizen_nagoya/items/a7e634a996cdd02bc53b

小川メソッド　覚え（書きかけ）
https://qiita.com/kaizen_nagoya/items/3593d72eca551742df68

DoCAP（ドゥーキャップ）って何ですか？
https://qiita.com/kaizen_nagoya/items/47e0e6509ab792c43327

views 20,000越え自己記事一覧
https://qiita.com/kaizen_nagoya/items/58e8bd6450957cdecd81

Views１万越え、もうすぐ１万記事一覧最近いいねをいただいた213記事
https://qiita.com/kaizen_nagoya/items/d2b805717a92459ce853

amazon 殿堂入りNo1レビュアになるまで。仮説(102)
https://qiita.com/kaizen_nagoya/items/83259d18921ce75a91f4

100以上いいねをいただいた記事16選
https://qiita.com/kaizen_nagoya/items/f8d958d9084ffbd15d2a

水道局10年(1976,4-1986,3)を振り返る
https://qiita.com/kaizen_nagoya/items/707fcf6fae230dd349bf

小川清最終講義、最終講義（再）計画, Ethernet(100) 英語(100) 安全(100)
https://qiita.com/kaizen_nagoya/items/e2df642e3951e35e6a53

＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
This article is an individual impression based on my individual experience. It has nothing to do with the organization or business to which I currently belong.
Este artículo es una impresión personal basada en mi experiencia personal. No tiene nada que ver con la organización o empresa a la que pertenezco actualmente.

文書履歴(document history)

ver. 0.01 初稿 20180318
ver. 0.04 URL追記　20230226

最後までおよみいただきありがとうございました。

いいね　💚、フォローをお願いします。

Thank you very much for reading to the last sentence.

Please press the like icon 💚　and follow me for your happy life.

Muchas gracias por leer hasta la última oración.

Por favor, haz clic en el ícono Me gusta 💚 y sígueme para tener una vida feliz.

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up

NuSMV入門 ４日で学ぶモデル検査 初級編

４日で学ぶモデル検査 初級編

導入

sample

Qiita on NuSMV

参考文献

文書履歴(document history)

最後までおよみいただきありがとうございました。

Thank you very much for reading to the last sentence.

Muchas gracias por leer hasta la última oración.

NuSMV入門４日で学ぶモデル検査初級編

４日で学ぶモデル検査　初級編