🐙
NuSMVと形式手法について学んだことまとめ
形式手法とは
- ソフトウェアやハードウェアの設計や開発において使用される手法の一つ。
- 数学的なモデルや形式的な言語を使用してシステムの仕様を明確かつ厳密に表現し、設計や実装の段階でのエラーや不備を最小限に抑えることを目指す。
- プログラムやシステムの信頼性向上や品質確保に寄与することが期待される
利用事例
- NASAなどでよく利用され、レクサス車の暴走事故の際にも事故原因の分析に形式手法が利用されたそう。
- その他事例は下記資料の付録(10) ケーススタディに記載あり。
形式手法に関する資料
- 師匠に形式手法を教えてもらった資料
古典論理とは
自然演繹とは
NuSMVを使って形式手法をトライ
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)
終わりに
- 検査式の書き方は、ドモルガンの法則しかり、書き換えができるため、いくつかの書き方ができる。
- 検査式が間違っていた場合、正しく検査できないため、検査式が適切かを検査する手法もあるそう。
Discussion