大規模複雑化した組み込みシステムのための障害診断における形式手法の適用事例報告

信州大学工学部
会津大学コンピュータ理工学部
准教授 岡野浩三
教授 北道淳司
okano@cs.shinshu-u.ac.jp
kitamiti@u-aizu.ac.jp
6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

1

故障原因診断WGの活動• 近年，大規模複雑化した組み込みシステムにおいて，ソフトウエアを起因とする障害が発生する• ソフトウエアの原因調査は十分と言えない，障害に対する製造者の説明責任が発生• 初動調査から設計・開発へのフィードバックにいたるまでの故
障原因診断に調査と提言を行う
IPA/SECとJASAによる 障害原因診断WG が発足(2014.04)
http://www.ipa.go.jp/sec/about/system.html
6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

2

事後V＆Vの概要と形式手法の位置付け• 障害発生原因究明に関するV(Verification)とV(Validation)が必要• 故障箇所を特定するための手段の一つとして，形式手法の・形式的モデリング・モデル検査手法が適用できないか検討

モデルの階層的表現による理解
 システム要求仕様のモデル化
 システム機能のモデル化

初動調査のガイドライン
 組込み系の調査マニュアル

ハザード分析 STAMP/STPA FTA、FMEA、 HAZOP

障害再現手法(ﾃｽﾄﾍﾞｯﾄﾞ) シミュレーターによる模擬実行 故障注入6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

仮説生成

仮説検証

障害箇所特定 障害箇所特定・切り分け手法、ログ分析
 ソフトウェア検証手法 （形式検証、モデル検査ツール等の調査、適用)

フィードバック
障害事例の分析・整理、教育への反映
 STAMP/CASTによる体系的な解釈
 教育コンテンツ

整理・データベース化

報告書と提言3

適用事例：化学プラントシステム

6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University4

溢水防止のための機能と発生した障害• アラートレベル（40cm)を越えると– 5秒間排出弁を開、同時に15秒間（含む5秒間）は新たな開指示を受け付けない• 運転員の指示で、上記と同じ排出弁の操作を行う• 運転員の指示は、常に優先する（15秒間の禁止区間でも受け付ける。自分自身の過去の指示に対しても優先する）• 発生した障害：– センサがオンで、緩和期間をすぎているのに排水できない– マニュアルの操作も受け付けない
6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

5モデリング１：ディレイタイマwith Reset• 入力 in 立ち上がり– 出力 out 0： 指定された時間d だけ１を出力– 出力 out 1: 何も変化無し

R1delay• 入力リセット reset 立ち上がり– 出力 out 0： 何も変化無し– 出力 out 1: 出力0• リセット後はin 立ち上がりで受け付け

6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

6

モデリング２：制御システム（Design A）
Manual trip
from controlroom
Input M4

R115s

ORT2_outAND

15s

Capacity
Alert

T1.Out1

Input C2
In.C2
手動動作のときは強制排水開始の直後に15秒間全体的にセンサ入力の伝達を禁止、を意図している

6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

7

UPPAAL を用いたModelA
UPPAAL
時間オートマトンのモデル検査
シミュレーション– モデル検査• モデル（有限状態遷移）• 時相論理式• しらみつぶしに検査
6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

8

システムにおいて成立する性質• 通常の形式手法では，システムにおいて成立してほしい性質をモデル上で，成り立つか議論する• ここでは，発生した障害の否定をシステムにおいて成立してほしい性質と考える → モデル検査に持ち込む• 排水が抑制されていなく、かつ、水位レベルセンサが警告レベルの状態であるときに、いつか「排水モード」になるか• (In.C2 and T2_out == 0) --> T1.Out1
以下の(UPPPAAL上の)略記
6/12/2015A□ ((In.C2 and T2_out == 0) imply A◊ T1.Out1)

Software Laboratory Department of Computer Science & Engineering Shinshu University

9

モデル検査モデル と 検証性質を与え• モデル検査は– モデル上で検証性質が成り立つかを網羅的かつ論理的に調べる– 反例（CE）はバグ同定に役立つトレース情報

TargetSystemSpecifications

6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

ModelProperty(Query)

Model
Checkingvalid

not valid(end)
CE10

検証結果
• 性質Ｐ は成立しないことがモデル検査で確認できる＝障害発生
ツールが出力する反例を障害診断に利用する

6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

11Design A
Manual trip
from controlroom
Input M4

m4
R1

out_timer1
15s

ANDOR

1
5s

Capacity
Alert
Input C2
inputsoutc2
6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University12

反例をモデル上で追跡する
初期状態は0
step

C2 on

m40

c20

inputs0

out_timer10

out0

action0c2 onOn(アラート)
は1に1010000sec

20110

10sec35sec 内にm4 on

01111
m4 on

41111

10sec

51110

15sec

6
これ以降水位レベルは異常値だが立ち上がりエッジが検出で7きないので出力が1にならない

6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

01

100
forever

01

100

13

反例の解析＝障害診断
R
Input M4

115s

OR

Input C2AND

15s

• 最初の5秒の緩和操作の間に、再度、運転員からの緩和指示が出た場合、15秒の操作禁止はリセットされるが、そのとき、水位がアラート越えの状態に留まっていた場合、AND出力は、0→１に立ち上がるが、5秒タイマは動作中で、これを受け付けない。5秒経過後も、AND出力が1で継続（水位アラート状態）の場合、AND出力は、1のままなので、5秒タイマは駆動されない。
• この状態で、運転員が緩和指示を出しても受け付けなくなる（運転員優先の逸脱）
146/12/2015
障害原因が診断された
Software Laboratory Department of Computer Science & Engineering Shinshu University

Design B (改善デザイン)
Manual trip
from controlroom
Input M4

15s

AND

OR

1

OR5s

Capacity
Alert
Input C2115s

6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

運転員指示を常に優先ため人間操作系統のマージを最後に行う

15

Design Bに対するUPPAAL Model

6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University

16

DesignBに対する検証結果
Design Bでは性質Pが成立
Design Bでは性質Pに関する故障の原因が取り除かれたと解釈できる

6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University17

まとめ• 故障原因診断WG，事後V＆Vとその中の形式手法の位置付け• 化学プラントシステムを例に形式手法を用いて，モデリングおよびモデル検査による障害診断の例を示した．
• 通常，設計初期の抽象モデルへの形式手法の適用は多い．故
障原因診断では，発生した障害，実際の開発物から形式手法の適用が始まる．参加者のご経験，ご意見を伺いたい

6/12/2015
Software Laboratory Department of Computer Science & Engineering Shinshu University18