シミュレーションを利用したモデル検証手順－ＳＰＩＮの場合

■シミュレーションを利用したモデル検証手順－概要

　動作させてチェックするのでは、チェックしきれないような場合、モデルを作成し、シミュレーションを利用して検証するという
モデル検証が行われる（というふうに学者さんは考えている）。

　このモデル検証では、性質を調べる。性質には
　　　　到達可能性
　　　　進行性
　　　　安全性
　　　　応答性
　　　　不変性
　などがある。ＳＰＩＮで調べる場合、このうち、到達可能性、進行性、安全性（デッドロックとライブロック）を調べることになる。
　これらについて、正常ケースと、非正常ケースについて確認し、さらに成り立つはずのない振る舞いが起こるかどうか確認する。

　以下、正常ケースと、そうでないケースに対して、ＳＰＩＮでの調べ方をみていく。

---

■シミュレーションを利用したモデル検証手順－ＳＰＩＮの場合


・正常ケースが起こることを確認
　　　　インタラクティブシミュレーターを利用する
　　　　　　　　assertを挿入し、反例が起きるか？（反例トレース分析）
　　　　　　　　ＬＴＬ式を利用する（進行性検証）

・（非正常も含め）すべての振る舞いがシミュレートできることを確認
　　　　シミュレーション利用
　　　　　　　　ランダムシミュレーションの利用
　　　　　　　　インタラクティブシミュレーションの利用
　　　　反例の利用
　　　　　　　　デッドロック検証・ライブロック検証
　　　　　　　　assert(false)の挿入（反例トレース分析）
　　　　ＬＴＬ式、assertの利用
　　　　　　　　成り立つはずのない振る舞いはしていないか？
　　　　　　　　非正常のケースも動いているか

以下、上述したＳＰＩＮでの各検証方法について、詳しく見ていく

---

■ＳＰＩＮでの各検証方法

・デッドロック検証
　強い公平性と弱い公平性によって、検証方法が異なる。
　　　弱い公平性：With Weak Fairnessにチェック
　　　強い公平性：ＬＴＬ式で記述

・ライブロック検証
　“Non-Progress Cycles"を設定し、“progressN” (N = 1, 2,…)ラベルを貼る

・進行性検証
　　次のLTL論理式の検証により実施　[](p1 -＞ ＜＞ p2) && [](p2 -＞ ＜＞ p3)
　（上記＜＞は、本当は半角）

・反例トレース分析
　　安全性検証時の反例トレース：最終状態で停止
　　　　アサーション違反（SafetyのAssertionsにチェックすること）、
　　　　デッドロック発生（デッドロック検証）、
　　　　不変条件の不成立（LTL式で、[]p pは不変条件として確認）

　　活性検証時の反例トレース：活性違反サイクル
　　　　ライブロックを起こす無限ループなど（ライブロック検証）

---

こんなところかな・・・あとで、一部加筆修正するかも。