🐙

NuSMVと形式手法について学んだことまとめ

2023/12/11に公開

形式手法とは

  • ソフトウェアやハードウェアの設計や開発において使用される手法の一つ。
  • 数学的なモデルや形式的な言語を使用してシステムの仕様を明確かつ厳密に表現し、設計や実装の段階でのエラーや不備を最小限に抑えることを目指す。
  • プログラムやシステムの信頼性向上や品質確保に寄与することが期待される

利用事例

  • NASAなどでよく利用され、レクサス車の暴走事故の際にも事故原因の分析に形式手法が利用されたそう。
  • その他事例は下記資料の付録(10) ケーススタディに記載あり。

http://formal.mri.co.jp/items/docs/フォーマルメソッド導入ガイダンスv1.0.pdf

形式手法に関する資料

  • 師匠に形式手法を教えてもらった資料

https://qiita.com/henri_t/private/ab92565a3f2188cabcde

古典論理とは

https://tmc-connected-company.atlassian.net/l/cp/kQcBVHRK

自然演繹とは

https://ja.wikipedia.org/wiki/自然演繹

NuSMVを使って形式手法をトライ

NuSMVとは

https://qiita.com/kaizen_nagoya/items/49fce418443f704ffec9

インストール方法

  • 以下のサイトの手順通りに実行していき、設定の「プライバシーとセキュリティ」→「セキュリティ」で解除すると使えるようになる

https://wwu-pi.github.io/tutorials/lectures/lsp/040_install_nusmv.html

例題

形式手法を使うと良いというケースステディを用いてNuSMVを使ってみる
NuSMV例題

実行結果

このシステムは1.306エポックでダウンすることがわかる

  -> State: 1.306 <-
    interrupt_A = TRUE
    interrupt_B = TRUE
    interrupt_C = TRUE
    timer_A = 1
    timer_B = 1
    timer_C = 1

smvのコード例

MODULE main
VAR
  interrupt_A: boolean;
  interrupt_B: boolean;
  interrupt_C: boolean;

  timer_A: 1..9;
  timer_B: 1..7;
  timer_C: 1..5;

ASSIGN
  init(interrupt_A) := FALSE;
  init(interrupt_B) := FALSE;
  init(interrupt_C) := FALSE;

  init(timer_A) := 2;
  init(timer_B) := 4;
  init(timer_C) := 1;

  next(interrupt_A) :=
    case
      timer_A = 9 : TRUE;
      TRUE        : FALSE;
    esac;

  next(timer_A) :=
    case
      timer_A < 9 : timer_A + 1;
      TRUE       : 1;
    esac;

  next(interrupt_B) :=
    case
      timer_B = 7 : TRUE;
      TRUE        : FALSE;
    esac;

  next(timer_B) :=
    case
      timer_B < 7 : timer_B + 1;
      TRUE       : 1;
    esac;

  next(interrupt_C) :=
    case
      timer_C = 5 : TRUE;
      TRUE        : FALSE;
    esac;

  next(timer_C) :=
    case
      timer_C < 5 : timer_C + 1;
      TRUE       : 1;
    esac;

SPEC
  AG !(interrupt_A & interrupt_B & interrupt_C)

検査式を以下のように置き換えることも可能

-- 検査式 --
SPEC !EF( interrupt_A = TRUE & interrupt_B = TRUE & interrupt_C = TRUE)

終わりに

  • 検査式の書き方は、ドモルガンの法則しかり、書き換えができるため、いくつかの書き方ができる。
  • 検査式が間違っていた場合、正しく検査できないため、検査式が適切かを検査する手法もあるそう。
GitHubで編集を提案

Discussion