近年，ソフトウェアを中心としたシステムに対する新たなハザード分析手法としてSTAMP/STPAが注目されている．
STAMP/STPAでは，システムに対するコントロールストラクチャを作成し，そこからハザードに至るシナリオおよび安全対策を導出する．STAMP/STPAは，FTAやETAといった従来型のハザード分析手法では識別ができないような，システムの機能間における認識の齟齬を要因としたハザードも識別することができるという特長がある．
一方で，システムの開発期間やコストが限られた中で効率的にシステムの品質を高めるためには，ハザードの発生確率と深刻度の積であるリスクに基づくシナリオの優先付けによる対策の検討が必要であると考えられる．
そこで本研究では，統計的モデル検査法を利用して，STAMP/STPAで導出されたシナリオに対するリスクを分析する手法について述べる．特に，STAMP/STPAにおけるコントロールストラクチャを形式化し，シナリオを形式的モデル上で表現する方法について提案する．
本研究では，鉄道における踏切制御システムを題材に手法を適用し，提案手法の評価を行った．その結果，STAMP/STPAで識別されたシナリオを形式モデルで表現し，シナリオの発生確率およびリスクを分析することができた．