研究課題
平成28年度は「モデル検査への拡張」と「ツール作成」を行った．【モデル検査への拡張】モデル検査では，状態推移モデル上で指定された時間に依存した性質が成立するかどうかを検査する．確定的なモデル検査は二分決定木（BDD）や充足可能性問題（SAT）を用いた条件を満たす状態を探索することが主な解析手法となるが，状態が確率的に推移するモデル上での検査は本質的に状態依存モデルの過渡解析に対応する．そのため，ここまでで確立した解析手法を確率的モデル検査に応用した．さらに，確率的モデル検査では特定の状態しか注目しないため，確定的なモデルチェッキング手法との組み合わせた過渡解析アルゴリズムの開発を行った．【ツールの作成】ツールの作成では「MRSPN/MRGP を定義する XML スキームの開発」，「解析ツールの実装」を行う．他のツールからの利便性を考慮して MRSPN/MRGP の定義を行うための XML スキーマ開発する．XMLスキーマは XML 文書中のタグなどの意味づけを行うものであり，このような定義はモデルの自動変換などに役立つ．本研究では，既存のペトリネットに対する XML に対して MRSPN を記述できるような拡張を行う．また，MRGP を定義するための XML の開発も行った．さらに，MRSPN 解析ツール JSPetriNet の実装を行った．MRSPN構造解析ツールは MRSPN を入力として，連続時間マルコフ連鎖の生成行列を出力する．また，連続時間マルコフ連鎖を数値的に評価するツールを R 上に作成した．
すべて 2016 その他
すべて 雑誌論文 (5件) (うち査読あり 5件) 備考 (1件)
日本信頼性学会誌
巻: 38 ページ: 340-349
Annals of Operations Research
巻: 244 ページ: 177-208
10.1007/s10479-015-1870-0
Proceedings of the 8th International Workshop on Software Aging and Rejuvenation (WoSAR 2016)
巻: - ページ: -
10.1109/ISSREW.2016.53
Proceedings of the 4th International Symposium on Computing and Networking (CANDAR 2016)
10.1109/CANDAR.2016.0041
Proceedings of the 7th Asia-Pacific International Symposium on Advanced Reliability and Maintenance Modeling (APARM 2016)
巻: - ページ: 415-422
https://github.com/rellab/JSPetriNet
