2016 Fiscal Year Annual Research Report
Development of Scalable Algorithms of MRSPN/MRGP Analysis for the Automation
| Project/Area Number |
26330028
|
|---|
| Research Institution | Hiroshima University |
|---|
Principal Investigator |
岡村 寛之 広島大学, 工学研究院, 准教授 (10311812)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | システム工学 / 性能評価 / 確率モデル / ペトリネット / モデル検査 |
|---|
| Outline of Annual Research Achievements |
平成28年度は「モデル検査への拡張」と「ツール作成」を行った．
【モデル検査への拡張】モデル検査では，状態推移モデル上で指定された時間に依存した性質が成立するかどうかを検査する．確定的なモデル検査は二分決定木（BDD）や充足可能性問題（SAT）を用いた条件を満たす状態を探索することが主な解析手法となるが，状態が確率的に推移するモデル上での検査は本質的に状態依存モデルの過渡解析に対応する．そのため，ここまでで確立した解析手法を確率的モデル検査に応用した．さらに，確率的モデル検査では特定の状態しか注目しないため，確定的なモデルチェッキング手法との組み合わせた過渡解析アルゴリズムの開発を行った．
【ツールの作成】ツールの作成では「MRSPN/MRGP を定義する XML スキームの開発」，「解析ツールの実装」を行う．他のツールからの利便性を考慮して MRSPN/MRGP の定義を行うための XML スキーマ開発する．XMLスキーマは XML 文書中のタグなどの意味づけを行うものであり，このような定義はモデルの自動変換などに役立つ．本研究では，既存のペトリネットに対する XML に対して MRSPN を記述できるような拡張を行う．また，MRGP を定義するための XML の開発も行った．さらに，MRSPN 解析ツール JSPetriNet の実装を行った．MRSPN構造解析ツールは MRSPN を入力として，連続時間マルコフ連鎖の生成行列を出力する．また，連続時間マルコフ連鎖を数値的に評価するツールを R 上に作成した．
|
