STAMP/STPAにおけるモデル検査の利⽤

2016年12⽉7⽇
⽇本ユニシス株式会社
総合技術研究所⻘⽊ 善貴

STAMP/STPAの⼿順概要
 STPAによるハザード分析の⼿順① Step0準備１︓
事故、ハザード、安全制約の識別② Step0準備２︓
コントロールストラクチャの構築③ Step1︓
UCA（Unsafe Control Action︓安全ではないコントロールアクション）の識別④ Step2︓
HCF（Hazard Causal factorハザード原因要因）の特定
1

ガイド
ワード

ガイド
ワード××

©2016 Nihon Unisys, Ltd. All rights reserved.

今回の提案（ This proposal ） Step2における HCF抽出をモデル検査を⽤いて⽀援する⼿法の提案
 コントロールアルゴリズムとプロセスモデルに注⽬してのハザード分析の⽀援

2©2016 Nihon Unisys, Ltd. All rights reserved.

プロセスモデルは重要（Process model is important）

コントロールアルゴリズム(Control Algorithm)＋プロセスモデル(Process Model)

コントロールアクション(Control Action)

3©2016 Nihon Unisys, Ltd. All rights reserved.

STEP２ ガイドワード（Guide Word）

4©2016 Nihon Unisys, Ltd. All rights reserved.

プロセスモデルの定義(Process model definition)

 コントローラが認識すべき被コントロールプロセスの状態を定義しなければならない なおかつ、そこから⽭盾を⾒つけなければならない

5©2016 Nihon Unisys, Ltd. All rights reserved.

モデル検査の利⽤(Use of Model Checking) プロセスモデルを網羅的に検証する（Exhaustive verification of the process model)
プロセスモデルの状態を網羅的に検査するには、モデル検査が有効と考える

6©2016 Nihon Unisys, Ltd. All rights reserved.

モデル検査を使うための課題（Problem）
 プロセスモデルのモデル化(Modeling of Process Model)
 コントロールアルゴリズムのモデル化(Modeling of Control Algorithm)

7©2016 Nihon Unisys, Ltd. All rights reserved.

適⽤事例

概要（Case Study）

 IPAが公開している資料「はじめてのSTAMP/STPA〜システム思考に基づく新しい安全性解析⼿法〜」にある
分析実施例「単線の駅中間踏切制御装置」
 警報開始センサA，Bは列車を検知すると踏切を鳴動させる．
 警報終止センサCは列車を検知すると踏切の鳴動を停止させる．
 警報終止センサCを通過した時点で，警報開始センサBをマスクする．
 警報開始センサBを通過した時点で，センサBのマスクを解除する．

Station １

Sensor A

Sensor C
8Sensor B

Station ２©2016 Nihon Unisys, Ltd. All rights reserved.

アクシデント・ハザード・安全制約
 アクシデント(Accident)
 列⾞と⼈もしくは⾞などが踏切内で衝突する

 ハザード(Hazard)
 列⾞が踏切通過中に警報が鳴動していない 安全制約(Safety Constraints)
 列⾞が踏切を通過中は、警報が常に鳴動している

9©2016 Nihon Unisys, Ltd. All rights reserved.

コントロールストラクチャ(Control Structure) コントローラ(Controller)は「踏切制御装置」(railroad crossing controller) 被コントロールプロセス(Controlled Process)が「センサABC」と 「警報機、遮断機」(AlarmSystem)
 「列⾞」(Train)はセンサに対する⼊⼒(Input)とする
10©2016 Nihon Unisys, Ltd. All rights reserved.

コントロールストラクチャ(Control Structure)(Railroad Crossing Controller)(Sensor A,B,C)(Train)(Alarm System)

11©2016 Nihon Unisys, Ltd. All rights reserved.

プロセスモデルの状態(State of Process Model)
センサ信号A～B

 コントローラからの視点
 センサについては信号の有無で⾒る
 警報⾳鳴動装置については、鳴動の有無で⾒る警報音鳴動装置

 制約
進⾏⽅向 左⇒右A通過回数>=C通過回数>=B通過回数
進⾏⽅向 右⇒左B通過回数>=C通過回数>=A通過回数
12©2016 Nihon Unisys, Ltd. All rights reserved.

コントロールアルゴリズム(Control Algorithm)

 センサA ⾮検知⇒検知／⾮検知 検知⇒検知／通過 通過⇒⾮検知

 センサC A通過回数＞C通過回数 かつ ⾮検知⇒検知／⾮検知 警報⾳鳴動装置
 センサA検知⇒鳴動開始
 センサC通過⇒鳴動停⽌

13©2016 Nihon Unisys, Ltd. All rights reserved.

モデル検査の実施(Model Checking) モデル検査ツール

NuSMV

 正常動作の検査(Inspection of normal operation)
 デッドロックしない、各駅へ到達する、鳴動する、マスクする 安全制約の検査(Inspection of Safety Constraints)
 安全制約︓列⾞が踏切通過中は警報が常に鳴動している
検査式︓列⾞が踏切通過中に警報が鳴動しないことは、決してない
14©2016 Nihon Unisys, Ltd. All rights reserved.

検査式の検討
 正常ならば、センサABCの通過回数、鳴動回数、鳴動停⽌回数は等しいはず
Number of Sensor A,B,C passage=Number of Alarm sounding= Number of Alarm stopping

通過１回

通過１回

通過１回

鳴動１回鳴動停⽌１回
15©2016 Nihon Unisys, Ltd. All rights reserved.

検証結果(Inspection Result)
検査式としては、「 A通過回数＝B通過回数＝C通過回数 かつ警報鳴動回数＜A通過回数」となることはない
SPEC AG!((Sens.A_CNT=Sens.B_CNT &Sens.B_CNT=Sens.C_CNT) &(RUNG_CNT < Sens01.A_CNT))

検証結果は、「満たされない」(Not satisfied)

16©2016 Nihon Unisys, Ltd. All rights reserved.

検証結果(Inspection Result) 反例を確認すると
 A通過回数＝２回
 B通過回数＝２回
 C通過回数＝２回
 警報鳴動回数＝１回
 警報鳴動回数＝１回

17©2016 Nihon Unisys, Ltd. All rights reserved.

反例解析(Counter Example)

センサA(sensor A)

センサC(sensor C)

鳴動
危険性がある(Ｒｉｓｋ)

警報機、踏切(Alarm System)(Alarm stopping)(Alarm sounding)18©2016 Nihon Unisys, Ltd. All rights reserved.

考察 接近した状態で２台の列⾞が運⾏されると，後発の列⾞が踏切を通過中に，もう先発の列⾞が警報を解除する可能性がある19©2016 Nihon Unisys, Ltd. All rights reserved.

まとめ(Conclusion)
 HCF抽出において、モデル検査を利⽤することにより、網羅的な検証の⽀援ができることを⽰した プロセスモデルの状態から、安全制約の検査式が記述できない場合は、再度検討が必要

20©2016 Nihon Unisys, Ltd. All rights reserved.