スライド作成ガイドライン何故モデル検査が必要なのか？ • 多くのソフトウェアが分散処理・並行処理を基 本としている – 複数の計算主体が並行動作をしながら共有資源 を用いて機能を実現している • システム全体が安全な動作をしない可能性が 高い – 資源を奪い合う競合状態に陥る可能性が高い – 非決定的な振る舞いについて、誤りがテストなど では現れない可能性が高い 1 非決定的な振舞 • 複数スレッド間の並列動作 • 複数機器間の並列動作 • ネットワーク環境の変化 2 複数スレッド間の並列動作 3 int a; (ロックは適切にとっているものとする．) スレッド間共有データ while (true) { if (a < 10) { a++; } } スレッド1 while (true) { a--; } a = 10; thread1.run(); thread2.run(); while (true) { b
