2001 Fiscal Year Annual Research Report
パラメータを持つ実時間システム仕様のモデル検査に関する研究
| Project/Area Number |
13780232
|
|---|
| Research Category |
Grant-in-Aid for Encouragement of Young Scientists (A)
|
| Research Institution | Osaka University |
|---|
Principal Investigator |
中田 明夫 大阪大学, 大学院・基礎工学研究科, 助手 (60295839)
|
|---|
| Keywords | 実時間システム / モデル検査 / 時間オートマトン / 時相論理 / パラメータ / 周期的システム |
|---|
| Research Abstract |
1.研究の目的
本研究では、実時間時相論理式で記述された実時間システムの要求仕様と時間オートマトンで記述された実時間システムの動作仕様が与えられ、双方に可変パラメータが記述されているとき、動作仕様が要求仕様を満足するための双方のパラメータ群に関する必要十分条件を自動的に導出するツールを開発する。そして、実用規模のシステム仕様に対して,本手法の有効性を評価する。ただし、実用規模のシステムはいくつかの時間オートマトンが通信しながら並行動作するモデルで記述されることが多い。そこで,開発するツールではそのような並行動作する複数の時間オートマトンが与えられたときにも,それらを全体の動きを表す単一の時間オートマトンに変換し,パラメータ条件を導出する。
2.本年度の研究成果
本年度においては、周期的実時間システムの記述モデル、周期時間オートマトンの状態sと実時間時相論理式RPCTLの各構文要素fの組(s, f)から、s以降の動作が性質fを満たすためのsの状態変数(パラメータ)に関する条件WPC(s, f)を再帰的に求めるアルゴリズムを考案した。当初の研究計画の、時間オートマトンからA-TSLTSというモデルに変換してからパラメータ条件WPC(s, f)を求める方針を変更し,直接時間オートマトンからWPC(s, f)を求めるようにした。この成果は国際会議FORTE2001にて発表した。また、いくつかの周期時間オートマトンが通信しながら並行動作するモデル、並行周期EFSM群から単一の周期時間オートマトンに変換するアルゴリズムを考案し、上記のWPC(s, f)を求めるアルゴリズムを考案し、ツールに実装した。一般にWPC(s, f)は限定子を含む一階述語論理式となるが、考案したアルゴリズムは、時間オートマトンの遷移条件は線形不等式の論理結合に限るという制限の下でパラメータ条件の限定子を除去および簡約化を行い、よりサイズの小さいパラメータ条件式を導出できるような工夫を行っている。ツールの性能評価に関しては国際会議CAV2002に投稿中である。
|
Research Products
(1 results)
