STAMP/STPA単線列車例題に対する時間オートマトンモデル検査の適用と考察

摘要

近年情報システムの大規模化複雑化にともない，情報システムの事故原因解明や事故そのものの事前防止策に注目があっまっている．システム理論に基づく事故モデルとして，従来は対応が困難である複雑なシステムに対する分析モデルにSTAMP（Systems Theoretic Accident Model and Processes）がある．STAMPを用いたアプローチでは障害の原因を，コンポーネントの故障や人間のエラーなどに限定せず，コンポーネント間やコンポーネントと人間の間のインターフェイスのミスなどの幅広い視野で分析する．STAMPに基づいた解析手法STPA（STAMP based Process Analysis）では，限定されたガイドワードを用いてハザードの同定を図る．モデルベースの障害診断にSTAMP/STPAの手法を取り入れ，モデル検査や制約指向の仕様検証などの形式手法と組み合わせることにより，より有効な障害診断の枠組みを得ることが期待できる．本稿ではSTAMP解析例題である単線踏切例題に対して動作モデルを時間オートマトンもデルとして構築し，モデル検査機Uppaalで解析したケーススタディについて述べる．また，これをもとにモデル検査技術とSTAMP/STPA手法との連携方法について考察を行う．