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

带参数的实时系统规格模型检验研究

• 批准号: 13780232
• 负责人: 中田 明夫
• 金额: $ 0.96万
• 依托单位: Osaka University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 2002
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13780232/
• 关键词: パラメトリックモデル検査; 実時間システム; 周期EFSM; 時相論理; 限定子除去; モデル検査; 時間オートマトン; パラメータ; 周期的システム

本研究では,並行周期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)以外の部分式の計算を回避する.次に,パラメタ条件に含まれる存在限定子を消去する.一般に,全称限定子を含む式は双対性を用いて存在限定子を含む式に変形できるが,その際式の長さが指数的に増大する可能性がある.このため式の長さが増大しないような十分条件を与え,それらを用いて式長が大きくならないように,全称限定子を消去する.最後に,パラメタ条件の式の特徴から簡約化のためのいくつかのヒューリスティックを導入した.これらを実装し,いくつかの例題に対して実験と評価を行い,その有効性を確かめた.

In this study, a method for simplifying and speeding up the inspection of parallel periodic EFSM is proposed. In this paper, we describe the behavior of the state transition and the behavior of the parallel periodic EFSM. Period EFSM is a kind of EFSM time expansion, a certain time (period), an initial state. Multiple periodic EFSMs operate in parallel. Parallel periodic EFSMs operate in parallel. Same name preceding shift operates simultaneously. Different name preceding shift operates independently. In addition, the state of EFSM is related to time constraints, including dynamic nature description,RPCTL(Real-time and Parametric extension of Computation Tree Logic), which is used in real time CTL. The proposed method of searching for parallel cycles EFSM is to derive the conditions for the on-the-fly and on-the-fly operations of a single cycle EFSM. The conditional expression of the condition WPC(s,f) is expressed in terms of the property f of the state s, and the partial condition WPC(si,fi) is calculated again. The calculation of high speed is very important. General conditions are derived and simplified. This method is based on the partial condition WPC(si,fi). The proposed reduction method is applicable to the main condition WPC(s,f) and the secondary condition WPC(s,f). When the condition WPC(s,f) is obtained, the results of partial expressions WPC(si,fi) are determined. When the results of partial expressions other than WPC(si,fi) are determined, the calculation of partial expressions other than WPC(si,fi) is avoided. Second, the existence of qualifier elimination is included in the condition. In general, all qualifiers are contained in the form of double pairs, and there are qualifiers in the form of double pairs. The length of this formula increases greatly and the condition of ten points increases greatly. Finally, the characteristics of the formula of the condition are changed from simplification to simplification. This is the case, and it's the case.

项目成果

森 亮憲, 中田 明夫, 東野 輝夫: "並行周期EFSMに対するパラメトリックモデル検査手法"電子情報通信学会論文誌D-I. Vol.J86-D-I, No.2. 75-87 (2003)

Akinori Mori、Akio Nakata、Teruo Higashino：“并行周期 EFSM 的参数模型检查方法”IEICE Transactions D-I，Vol.J86-D-I，No.2 (2003)。

Akio Nakata, Teruo Higashino: "Deriving Parameter Conditions for Periodic Timed Antomata Satisfying Real-Time Temporal Logic Formulas"Proc. of IFIP TC6/WG6.1 Int. Conf. on Formal Techniques and Distributed Systems(FORTE2001). 151-166 (2001)

Akio Nakata、Teruo Higashino：“导出满足实时时序逻辑公式的周期性定时 Antomata 的参数条件”Proc。