|
システムの性質は大きく2種類に分類できる。安全性と活性である。安全性のモデル検査には特別の仮定を必要としないが、活性のモデル検査では公平性と呼ばれる仮定を必要とする場合がある。
公平性のもとでの活性のモデル検査対象の論理式は"公平性 ⇒ 活性"の形をとる。モデル検査対象の論理式はBuchiオートマトンへ変換される。この変換は論理式の大きさに対しべき乗の計算と空間を必要とするため、公平性が大きくなるとBuchiオートマトンへの変換が実質不可能になり、モデル検査自体もできなくなる。
本研究では、"公平性 ⇒ 準公平性"を満たし、公平性より小さな論理式である準公平性を探し、"準公平性 ⇒ 活性"をモデル検査することで公平性のもとでのモデル検査を可能とする方法を提案する。すなわち、"公平性 ⇒ 活性"の代わりに、"公平性 ⇒ 準公性"と"準公平性 ⇒ 活性"をモデル検査することである。一般には、"公平性 ⇒ 活性"を簡単な命題計算により演繹できる2個より多くの論理式を生成し、それらをモデル検査することを行う。提案方法「分割統治に基づく活性のモデル検査法」をSuzuki-Kasami分散相互排除プロトコルが無排斥性を満たすことのモデル検査に適用することで有効性を確認した。無排斥性とは、際どい領域に入りたくなったどのプロセスも必ずそこに入ることのできるという性質である。
活性のモデル検査では、公平性に加え、ある種の不公平性の仮定も必要になることがある。たとえば、通信プロトコルAlternating Bit Protocol (ABP)の活性のモデル検査では、パケットの欠落が連続して起こり続けることは無い等の仮定を必要とする。提案方法は、このような不公平性の仮定も公平性と同様に扱えることができることがわかった。ABPの活性のモデル検査に適用することで有効性を確認した。
|
