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

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.