抄録

B-030
待ち行列理論による抽象化を用いたモデル検査手法の検討

組込みソフトウェアの複雑化・大規模化に伴い，開発上流工程での性能検証技術の必要性が高まっている。上流工程での検証技術としてモデル検査が注目されているが，時間に関する性能検証への適用には状態数爆発が発生しやすいという問題がある。本研究ではこの問題の解決方法として，検証モデルを待ち行列理論により抽象化することでモデル検査実行に要する状態数を削減する手法を検討した。モデル検査ツールDT-SPINを用いてATMの性能検証を題材とした評価実験を行った結果，従来手法と比べて状態数が削減し，提案手法の有効性を確認することができた。さらに，待ち行列の窓口数が多い場合には状態数削減の効果が高くなることがわかった。