パラメータを持つ実時間システム仕様のモデル検査に関する研究

Research Project

Project/Area Number	13780232
Research Category	Grant-in-Aid for Young Scientists (B)
Allocation Type	Single-year Grants
Research Field	計算機科学
Research Institution	Osaka University
Principal Investigator	中田明夫大阪大学, 大学院・情報科学研究科, 助教授 (60295839)
Project Period (FY)	2001 – 2002
Project Status	Completed (Fiscal Year 2002)
Budget Amount *help	¥1,500,000 (Direct Cost: ¥1,500,000) Fiscal Year 2002: ¥700,000 (Direct Cost: ¥700,000) Fiscal Year 2001: ¥800,000 (Direct Cost: ¥800,000)
Keywords	パラメトリックモデル検査 / 実時間システム / 周期EFSM / 時相論理 / 限定子除去 / モデル検査 / 時間オートマトン / パラメータ / 周期的システム
Research Abstract	本研究では,並行周期EFSMに対するパラメトリックモデル検査およびパラメタ条件簡約高速化の一手法の提案を行った.パラメトリックモデル検査は,与えられた状態遷移モデルがある性質を満たすためのパラメタ条件を導出する手法であり,本論文ではシステムの動作を記述した状態遷移モデルを並行周期EFSMで表現する.周期EFSMはEFSMの実時間拡張の一種であり,ある一定時間(周期)が経過すると初期状態へ戻るようなモデルである.複数の周期EFSMが並行動作する並行周期EFSMでは,同じ名前を持つ遷移は同期実行され,異なる名前を持つ遷移は独立に実行される.また,実時間EFSMの状態に対して,時間制約を含む動的性質を記述するための論理として,RPCTL(Real-time and Parametric extension of Computation Tree Logic)と呼ばれる実時間拡張CTLを用いる.提案するパラメトリックモデル検査手法では,並行周期EFSMをオンザフライ(on-the-fly)で単一周期EFSMに動的に変換し,パラメタ条件を導出する.パラメタ条件WPC(s,f)は,状態sで性質fが満たされるための条件式を表し,部分条件WPC(si,fi)を再帰的に計算することによって導出する.これらの計算を高速に行うためには,パラメトリックモデル検査で出力されるパラメタ条件のサイズを小さくするための簡約化手法が重要である.一般にパラメタ条件を導出した後に簡約化を行うと式のサイズが長大になり,簡約に時間を要する.そこで本手法では部分条件WPC(si,fi)を計算しながら,オンザフライで簡約化を行う.提案する簡約化法では,主にパラメタ条件WPC(s,f)の簡約化のために次の3つの手法を適用する.まず,パラメタ条件WPC(s,f)を求める際に,部分式WPC(si,fi)の結果によって全体の結果が決まる場合は,WPC(si,fi)以外の部分式の計算を回避する.次に,パラメタ条件に含まれる存在限定子を消去する.一般に,全称限定子を含む式は双対性を用いて存在限定子を含む式に変形できるが,その際式の長さが指数的に増大する可能性がある.このため式の長さが増大しないような十分条件を与え,それらを用いて式長が大きくならないように,全称限定子を消去する.最後に,パラメタ条件の式の特徴から簡約化のためのいくつかのヒューリスティックを導入した.これらを実装し,いくつかの例題に対して実験と評価を行い,その有効性を確かめた.