Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
モデル検査入門
Search
r1ru
August 13, 2024
2
160
モデル検査入門
r1ru
August 13, 2024
Tweet
Share
More Decks by r1ru
See All by r1ru
ImaginaryCTF 2025 stillerer-printf (魔女のお茶会 #8)
riru
0
360
Infer入門
riru
4
1.7k
Formal Development of Operating Systems in Rust
riru
1
650
プログラム検証入門
riru
6
2.6k
Symbolic model checker from scratch in Rust
riru
1
830
WasmOS: Wasmを実行する自作Microkernel
riru
0
810
Featured
See All Featured
Navigating Team Friction
lara
189
15k
How GitHub (no longer) Works
holman
315
140k
jQuery: Nuts, Bolts and Bling
dougneiner
64
7.9k
Being A Developer After 40
akosma
91
590k
Chrome DevTools: State of the Union 2024 - Debugging React & Beyond
addyosmani
7
890
StorybookのUI Testing Handbookを読んだ
zakiyama
31
6.2k
Site-Speed That Sticks
csswizardry
11
870
Java REST API Framework Comparison - PWX 2021
mraible
33
8.8k
How to train your dragon (web standard)
notwaldorf
96
6.3k
"I'm Feeling Lucky" - Building Great Search Experiences for Today's Users (#IAC19)
danielanewman
229
22k
YesSQL, Process and Tooling at Scale
rocio
173
14k
4 Signs Your Business is Dying
shpigford
185
22k
Transcript
モデル検査入門 1 Riru Oda @ri5255 セキュリティ・キャンプ2024 全国大会 LT
2 Agenda • モデル検査とは? • 文献案内
3 モデル検査とは? プログラムが仕様を満たしてることを自動的に検証する技術
4 モデル検査とは? 例) 2つのスレッドp, qが一つの共有変数xを読み書きする While (true) { x =
x + 1; x = x – 1; } 仕様: 𝐴𝐺(𝑥 < 2) 全て(All)の実行パスで常に(Globally) x < 2が成り立つ
5 モデル検査とは? 例) 2つのスレッドp, qが一つの共有変数xを読み書きする While (true) { x =
x + 1; x = x – 1; } 仕様: 𝐴𝐺(𝑥 < 2) 全て(All)の実行パスで常に(Globally) x < 2が成り立つ
6 モデル検査とは? 例) 2つのスレッドp, qが一つの共有変数xを読み書きする 仕様: 𝐴𝐺(𝑥 < 2) 全て(All)の実行パスで常に(Globally)
x < 2が成り立つ While (true) { lock(“mutex”) x = x + 1; x = x – 1; unlock(“mutex”) }
7 モデル検査とは? 例) 2つのスレッドp, qが一つの共有変数xを読み書きする 仕様: 𝐴𝐺(𝑥 < 2) 全て(All)の実行パスで常に(Globally)
x < 2が成り立つ While (true) { lock(“mutex”) x = x + 1; x = x – 1; unlock(“mutex”) }
8 モデル検査とは? モデル検査器 プログラム記述 + 仕様 Ok 反例
9 Agenda • モデル検査とは? • 文献案内
10 文献案内 • TLA+についての本 • 様々なシステムをモデル検査 で検証する(例: MapReduce) • とりあえず使ってみたい人向け
11 文献案内 • 並行計算、分散システム + モデル検査に関する本 • SPINを使う
12 文献案内 • モデル検査の理論の本 • 理論を知りたい人向け
13 文献案内 • モデル検査器の実装に関する本 • 実装してみたい人向け https://www.youtube.com/live/96u4dBAOzao?t=9802s
14 まとめ • 形式手法のモチベーションは「ある種のバグが無いことを理論的に保証する」こと • 数理論理学 (論理学、計算論 など) と深いつながりがある、理論的にも奥が深い分野 形式手法に入門しよう!!