日本ソフトウェア科学会第 30 回大会 (2013 年度) 講演論文集

人為的欠陥の意味と耐性解析
永藤 直行

渡部 卓雄

人為的欠陥に対する作業手順の耐性をモデル検証の手法を用いて解析する枠組を提案する．多くの場合，作業手順には人為的欠陥による誤り検出や復旧のためのタスクが埋め込まれている．作業手順の信頼性を保持するためには検出や復旧タスクの有用性を検証する必要がある．有用であることを示すために, 耐性を解析する時には欠陥を埋め込む．
ここでは，作業について訓練された人間が引き起こす人為的欠陥の分類をもちい，各分類の特徴の意味を遷移システ
ム上で定義する．解析時には，欠陥を含まない振舞モデルを人為的欠陥の意味にしたがって変換し，そのモデルをモデル検証の手法をもちいて検査する．検査する性質は作業手順の目的の否定となる．もし反例が見つかれば，そのときにはその作業手順は埋め込んだ人為的欠陥に対して耐性がないと云うことができる．

内面から考察している．しかし，我々はいま思考の結1 はじめに果として得られる人間の出力としての行動に興味が工業プラント，飛行機，病院など多くの状況で作業ある．Discrete Action Classification(DAC) [10] は出手順が存在している．手順の信頼性は，高度に訓練さ力として (システムへの入力として) の正しくない行れた人間のスキルだけでなく手順自身がディペンダブ

動を分類し特徴づけている．訓練を受けた人間が起こルであることによって達成される．よく訓練された人

す人為的欠陥となる正しくない行動を分類している．

間でも人為的欠陥を引き起こし得るので，作業手順がその分類を以下に示す．人為的欠陥は omission と人為的欠陥による誤りを発見し，修復するように設計

commission の 2 つに分類され，commission faults

されていなければならない．

はさらに詳細に分類されている．

人為的欠陥は，悪意をもって行われるかや故意によるかと云う視点から分類がなされている ( [1] の図.6
参照)．本稿では故意に悪意のある人為的欠陥は対象としない．良く訓練を受けた人間が運用時に不作為に引き起こす人為的欠陥を対象とする．
心理学的な視点で思考のレベルによる人為的欠陥の分類がなされている ( [8],pp.53–96 参照)．思考のレ
ベルを skill-base, rule-base, knowledge-base にわけ，

• Faults of Omission:– omits entire task
– omits a step in a task
• Faults of Commission:– Selection fault:

selects wrong control,

mispositions control or, issues wrong command and information.
– Sequence fault: out of order.
– Timing fault: too early or too late.

Semanitcs of Human-Made Fault and Robustness
AnalysisNaoyuki Nagaotu, 有限会社プレシステム, PRESYSTEMS Inc..
Takuo Watanabe, 東京工業大学情報理工学研究科計算工学専攻, Department of Computer Science, Graduate School of Information Science and Engineering,Tokyo Institute of Technology.

– Qualitative fault: too much or too little
本論文は DAC にしたがって議論する．

Omission fault は正しいタスクを何らかの理由で行わない人為的欠陥である．さらに，タスク全体を行わないか，タスクの一部を行わないかで分類されている．我々は，タスクはアトミックであると仮定してモデル化を行う．よって，”omits entire task” について意味を定義し， ”omits a step in a task” は対象としない．Commission fault は何かタスクは実行しているが正しくない何かをしてしまう人為的欠陥である．我々は commission fault のうち selection

fault と sequence fault について，その意味を定義す
る．利用するモデル検証器のモデリング言語では時間の概念を持っていないので timing fault は対象としない．また，タスクの質に関する形式化はここでは対象としない．よって， qualitative fault は対象としない．

Krishnan [4] は多重化されたシステムにおける欠陥
を omission fault と value fault と addition fault であるとしている．彼の omission fault は，同期を取るようなシステムにおいてメッセージを送信しない欠陥としている．Value fault は期待される動作とは異なる動作をする欠陥としている． Addition fault は
期待されないメッセージを送信する欠陥であるとして



Scenario

1. A patient gives a clerk in the room his idcard.
2. The clerk makes the receipt system read theid card.
3. The system gives the clerk two receipt sheetsand gives a nurse labels.
4. The clerk gives the patient one of two andgives a nurse another.
5. The nurse prepares tubes.
6. The nurse makes the system read the labels.
7. The nurse puts the labels on the tubes.
8. The system calls a receipt id.
9. The nurse confirms the name on the labelswith a name on the sheet.
10. The nurse receives a sheet from the patient
after having a seat.
11. The nurse compares the name on the sheet,given by the clerk, with his name.
12. The nurse extracts blood samples from thepatient.
13. The nurse takes the blood samples to a lab.

いる．その意味を CCS における refinement 関数を
図1

採血手順の例

用いて形式化し，耐性システムの特徴を捉えようとしている．この他にも欠陥を定義して partial model

ある．人為的欠陥が起こると重大な事故を引き起こ

checking や高階論理と型を元に議論した報告もある

すであろうと予測されるタスクが与えられるとして，[9] [2] [3]．我々は，システムの耐性ではなく，人間がそのタスクのところに欠陥を埋め込む．埋め込んだモ

動作主体となる作業手順の耐性について議論する．

デルに対して，作業手順の目的をあらわした時相論理

先に述べたように， DAC の分類のうち ”omits entire task†1 ” と ”selection fault” と ”sequence fault”

式に反する例をモデル検証を利用して解析する．何らを対象に，その意味をプロセス代数 CCS [5] の上で定てその作業手順は耐性を持っていないと判断できる．

義する．期待される動作であるタスクはアクションと簡単な適用例として採血の手順を対象にした検証結

してあらわすことにする．Omission fault は期待さ果を示す．

かの反例が見つかった時には埋め込んだ欠陥に対しれるタスクをするかどうかであるので，対応するアク

本稿は以下のように構成される． 2 節では提案手ションを含むプロセス式と含まないプロセス式の選択法が必要となることを例で示す． 3 節ではモデルの合成であらわす． Selection fault は期待されないタ

記述と手順の目的を記述するための体系について述

スクに対応するアクションを含むプロセス式との選択

べる． 4 節では人為的欠陥の形式的な意味を与える．

合成であらわす． Sequence fault はタスクに対応し

5 節でモデル検証を利用する枠組について述べる．

たプロセスの同期合成を用いてあらわす．

最後に 7 節で本研究の概要をまとめ将来の展望につCCS 上で定義された意味はモデルに欠陥を埋め込いて述べる．

むために利用される．モデルは期待されたタスクの列としての作業手順をプロセス式であらわしたもので

2 動機づけ作業手順の例として血液検査の一部をなす採血の手†1 以降では，これを omission fault と呼ぶことにする．

順 (図.1) をあげる．実際には分岐を含んだ複雑なもの

になっている．ここでは，そのうちのひとつの作業の

CCS のサブセットを利用する．また，作業手順の目

流れを抽出したものを示している．この手順は，患者的を記述するために有限列についての線形時相論理(patient) が採血室に到着し受付で id カードを提示すを利用する．

る所から始まっている．受付係 (clerk) は id カードを受け取りそれを受付システム (receipt system) に

3. 1 プロセス代数

読み込ませる．受付システムは血液検査のオーダのCCS はプロセス代数のひとつの体系である．シー

データベースを検索し，該当するオーダがあれば受付

ケンシャルな振舞をする複数のプロセスの同期通信

表 (receipt sheet) 2 枚とラベル (label) を発行する．

を元にした体系である．同期通信は入力アクションと受付表には受付番号と患者氏名と id が印刷されてい出力アクションという 2 種類のアクションの実行でる．受付係は 1 枚を患者に渡し，もう 1 枚とラベル生じる．入力アクションは適当な名前がつけられる．

(label) を所定の位置に受付順に置く．看護士 (nurse)

名前の集合を A とする．a ∈ A と同期する出力アクは採血管 (tube) を準備する．準備が済んだらラベル

ションを a で与える．A は A と互いに素であるとすを受付システムに読み込ませ，ラベルを採血管に貼る．A ∪ A の要素を α, β, · · · であらわすことにする．

る．受付システムは対応する受付番号を呼び出す．看プロセス式の構文を以下のように与える．E, F は護士はラベル上の患者氏名と受付表の患者氏名を画面の名前で確認する．呼び出して椅子にかけた患者から名前を名乗ってもらい，それと受付係から受け取った受付表の氏名を比較する．それが一致していたなら
ば，患者から血を採取する．採取した採血管と受付表を束ねてそれを検査室に看護士が持って行く．
図.1 の手順において重要なタスクは 9 と 11 である．2 回同じものを確認すれば人為的欠陥を回避できプロセス，a は名前とする．

• 出力アクション (a(e1 , · · · , en ) : E) はプロセスとする• 入力アクション (a(x1 , · · · , xn ) : E) はプロセスとする• E と F の選択合成 E+F はプロセスとする• E と F の同期合成,E|F はプロセスとする• プ ロ セ ス 定 数 P (x1 , · · · , xn ) も プ ロ セ ス で ，def

る可能性があるとして導入している．採血の前にこP (x1 , · · · , xn ) = E によって与えられるの 2 つのタスクのいずれかで取り違いが発見される• 条件式 if (b) (E) (F ) もプロセスとするように設計されている．患者の取り違いを発見したと

ここで，x1 , · · · は V 上の変数，e1 , · · · は V の式，bきのリカバリの手順が存在するはずであるが，この手順では規定していないのでリカバリを表す単純なタは V 上の論理式とする．STOP という特別なプロセスを導入する．†2 ．何もしないと云う特別な意味を

スクを仮定して 6 節で述べる振舞モデルを作成する．

持つ．各意味は CCS と同じであるのでここでは省略

複数の患者の採血をひとりの看護士が同時に行ってする．

いたとして，何らかの理由により採血管や受付表やラベルが入れ替わってしまっている状況を考える．その3. 2 有限列上の LTL

ような状況でいずれかのタスクを看護士が怠ってし作業手順の目的をあらわすために線形時相論理

まったとしても発見できるかどうか検証する．看護士

LTL をもちいる．作業手順は初期状態をもち，有限がいずれかのタスクで起こす人為的欠陥について耐列 σ = s0 s1 · · · sn であると仮定する．有限列 σ の性があれば，高い信頼性を保証することになる．

長さを |σ| と書き， |σ| は n + 1 とする．有限列 σの i で始まるサフィックスを σ i.. = si · · · sn として，

3 準備

i 番目の状態を σ i と書くことにする．

この節では本稿で利用する理論体系について述べ作業手順の目的を以下ように再帰的に定義される

る．期待される手順をあらわすモデルを記述するた†2 CCS では ZERO としているが，本稿では STOPとする．

めと人為的欠陥の意味を定義するために Milner の論理式で与えることにする．φ, ψ は時相論理式とする．そのとき，

4. 1 作業手順の構造
人為的欠陥の形式的な意味を定義する前に作業手• 状態論理式 p は時相論理式

順の構造について考える．作業手順はタスクの列の集• 時相論理式の否定 ¬ϕ は時相論理式

合と見なす．タスクはそれを行う主体と対象を持つ．

• ϕ ∨ ψ と ϕ ∧ ψ は時相論理式

タスクが実行された時には主体から対象にメッセー• 2 ϕ, 3 ϕ, ◦ ϕ, ϕ U ψ は時相論理式

ジが送信される．メッセージによりある種の情報がである．V 上の変数 x, y, z, · · · とする．状態論理式

伝達される．メッセージはその送信と受信によって生

p は V 上で構成される．もし p が s で真となるとき起される．また，タスクは互いに依存関係が存在し，

s[|p|] = tt となる．
．また， tt と ff はそれぞれ真とその依存関係はタスク間の順序としてあらわされる．

偽を意味する．

ここで云うタスクはアトミックであると仮定する．

各時相論理式の有限列上の意味を定義する．もし有作業手順は 3 つ組 (C, T , O) によって特徴づけられ

限列 σ が ϕ を充たしている時， σ |= ϕ と書くことる．C は タスクの主体と対象の集合． T はタスクのにする．
σ |= p

あらわされる．たとえば， 図.1 の採血手順の例では，集合で，タスクの依存関係は O(⊆ T × T ) によって⇔|σ| 6= 0 and σ 0 [|p|] = tt,

σ |= ¬ϕ⇔|σ| 6= 0 and σ 6|= ϕ,σ |= ϕ ∧ ψ⇔σ |= ϕ ∧ σ |= ψ,σ |= ϕ ∨ ψ⇔σ |= ϕ ∨ σ |= ψ,σ |= Xϕ⇔σ 1.. |= ϕ,read id-card”, ”give clerk two sheets”, ”giveσ |= ϕUψ⇔∃ k s.t. σ k.. |= ψ andreceipt to nurse”,· · ·},for every j < k, σ j.. |= ϕ.
有限列の集合 T と時相論理式 ϕ が与えられたとして，全ての σ ∈ T について σ |= ϕ であるとき ϕ はT で妥当であると云う．
3. 3 プロセスと時相論理式の関係
プロセスは a(e) と a(x) によって値を送受信することができる．このとき e の評価値を x へ束縛する
単一の代入と見なすことにする．この代入はプロセ
スであらわされたモデルの状態を変更する．これをs[v/x] であらわすことにする．ここで，v は e の s
における評価値とする．同期の列は代入の列を生成し，さらに状態の遷移を生成すると考えることにする．たとえば，p を (x = y) とすると s[v/x][|x = y|]は v = s[v/x][|y|] となる．

4 人為的欠陥の意味
人為的欠陥の意味をプロセス代数で定義する．この形式化は人為的欠陥が起こるかも知れないタスクに対応するプロセスを生成する．

• C ={patient, nurse, label, receipt, clerk, tube,
laboratory},• T ={”give a clerk id-card”, ”make system• O ={(”give a clerk id-card”, ”make systemread id-card”), (”make system read id-card”,”give clerk two sheets”),· · ·}.
となる．
本稿では，耐性の解析をする時には実際の意味は考えていない．手順に現れるタスクは単なる記号であり，その実際の意味は状況によって異なる．作業手順の耐性を検証して得られた結果は記号としてのタスクからある状況で解釈が与えられたとして，意味を考えなければならない．

4. 2 人為的欠陥の埋め込み
人為的欠陥の意味を期待される作業手順のモデ
ルから人為的欠陥が埋め込まれた作業手順のモデルへの変換を示す．本稿では， 3 節で述べた体系の制約から omission fault と selection fault と se-quence fault を扱うことにする．作業手順の振舞モデ
ル W = (C, T , O) における欠陥タスクの集合 H が与えられたとする．
最初に omission fault について述べる．t ∈ H ，

H ⊆ T として，(t1 , t), (t, t2 ) ∈ O である各 t1 , t2 ∈ T

に つ い て ， {(t1 , t2 )} を O に 追 加 す る ．つ ま り

O

0

0

= O ∪ {(t1 , t2 )} と す る ．O に よ り 新 た に

WH = (C, T , O0 ) を得る．

と Task α1 | Task α2 であらわせる．この形式化をもちいて図.1 に埋め込んだモデルを図.2 に示す．

H = {”confirm label”, ”compare receipt”} と仮定

T = A ∪ A として，この変換を 3 節のプロセス代

している．

数であらわす．選択合成をもちいて

5 検証の枠組(α(e) : STOP ) + (STOP ))ここで α ∈ A ∪ A．

この節では欠陥を埋め込んだうえで，作業手順が目つぎに， selection fault について述べる．人為的を達成できるかどうか解析する枠組を与える．ロバ

的欠陥を起こすタスクの集合 H ⊆ T と期待されストネスは外的要因に依存した属性である．作業手順

0

ないタスクの集合 H * T が与えられたとする．
00t ∈ H, t ∈ H と して ，も し (t1 , t), (t, t2 ) ∈ O
00

で あ る な ら ば ，t を t で 置 き 換 え た (t1 , t ) と0

00のロバストネスを以下のように定義する．
定義 1 (Robustness) e をエラー状態をあらわす
論理式， ê 番目の状態はエラー， ϕ は目的をあ(t , t2 ) を得る．{(t1 , t ), (t , t2 )} を O に追加してらわす時相論理式とする．もし ê が σ 上に存在しO0 = {(t1 , t0 ), (t0 , t2 )} ∪ O と T 0 = H 0 ∪ T より，

σ ê.. |= 3ϕ ならば σ は e でロバストであるとして，

WH,H 0 = (C, T 0 , O0 ) を得るとしてこの変換を選択合

σ は (e, ϕ)-robust であるという．もし ϕ が W から成をもちいて得られるすべての状態列について妥当であるならば，00α(e1 ) : STOP + α (e ) : STOPと あ ら わ す．こ こ で T

0

W は (e, ϕ)-robust である．

= A ∪ A として，

この定義は直観的には状態列 σ がエラー状態から復α(e1 ), α0 (e0 ) ∈ A ∪ A．Omission fault と selection

帰して ϕ を充たすゴールに至ることができることを

fault をあわせて意味している．
00(α(e1 ) : STOP ) + (α (e ) : STOP ) + STOP )とすることができる．

ロバストネスを保証する技術について考える．このテクニックはエラーの発見とリカバリを含んでいる．

最後に sequence fault について述べる．t1 , t2 ∈ H

リカバリはエラーハンドリングとフォルトハンドリン

として，O は O 0 = {(t1 , t2 ), (t2 , t1 )} ∪ O となる．こグからなる．エラーハンドリングはエラーを一時的

00の O から WH = (C, T , O ) を得ることができる．

に解消することであり，この場合再びエラーが出現す

各 t1 , t2 ∈ H について 2 つのプロセスを定義する．

るかもしれない．フォルトハンドリングはファルトを

以下のようになる．ここではプロセス名をそれぞれ解消し，再びそのフォルトは起こらないようにする．

Task t1, Task t2 している．
def
Task α1 = (α1 (e1 ) : STOP ),本稿ではエラーハンドリングについて議論することにする．人為的欠陥は完全に解消することは難しいと

def

Task α2 = (α2 (e2 ) : STOP )ここで， T 0 = A∪A として， α1 (e1 ), α2 (e2 ) ∈ A∪Aとする．同期合成をもちいて以下のようなプロセスであらわせる．

Task α1 | Task α2omission fault, selection fault，sequence fault のいずれかが起こるとして，
defTask α1 = ((α1 (e1 ) : STOP

+α01 (e01 ) : STOP ) + STOP )Task α2def=((α2 (e2 ) : STOP
+α02 (e02 ) : STOP ) + STOP )考えられるからである．
ここで，リカバリを定義する．リカバリは直観的に
はエラーになった後でも期待される状態に復帰することとする．
定義 2 (Recovery) σ を状態列， e をエラー状態をあらわす論理式，r をリカバリ状態をあらわす論
理式とする．もし σ |= 2(¬ e) ∨ 3(e ∧ 3r) ならば σはリカバリ可能であるという．
いま， 2(¬ e) ∨ 3(e ∧ 3r) を e  r と書くことにする．
補題 1 () σ が与えられたとして，ei をエラー状態をdef

Task confirm label =((confirm label(name on display TaskConfLbl) :(if (name on label TaskConfLbl= name on display TaskConfLbl)(STOP )
(recovery label(name on display TaskConfLbl) :recovery label(name on label Nurse) :STOP )))+STOP )
def

Task compare receipt =((compare receipt(
name on display TaskCmpRecpt) :(if (name on receipt of patient TaskCmpRecpt= name on display TaskCmpRecpt)(STOP )
(recovery receipt(
name on display TaskCmpRecpt) :recovery receipt(
name on receipt of patient Nrs2 ) :STOP )))+STOP )
図2

def

Nurse2 =(receive receipt(
name on receipt for patient Nrs2 ) :(Task compare receipt(
name on receipt for patient Nrs2 )|Nurse1 ))def

Nurse1 =(extract blood :take sample to lab(name on receipt for patient Nrs2 ,name on label Nurse) :Nurse)
def

Nurse =
(give receipt to nurse(receipt id Nrs,
name on receipt Nurse) :give label(receipt id on label Nrs,
name on label Nurse) :prepare tube :make system read label :put label on tube(name on label Nrs) :(Task confirm label(name on label Nrs)
|N urse2))

人為的欠陥を埋め込んだ振舞モデル

補題 1 より，もし σ |= ¬3ϕ となる σ が存在してあらわす論理式， ri はリカバリされた状態をあらわす∧
論理式とする．このとき，もし σ rˆi .. |= ( i ri ) ∧ 3ϕ∧∧
かつ σ |= i (ei ri ) ならば σ |= ( i (ei ri )) ⇒ 3ϕ

る．これはリカバリできないエラー状態が存在することなる．

とを云っている．ゆえに，ゴールをあらわす論理式が証明 1 ei がエラー状態論理式， ri がリカバリ状態

与えらるとして，その否定を与えることでモデル検証

論理式とする．σ |= (ei  ri ) が σ 上で成り立つと仮の手法をもちいてリカバリ可能性が検証できる．

いると σ |= ¬(ei  ri ) となる ei が存在することにな

定する．

iﬀ

σ |= (ei  ri )6 Model Checking

σ |= 2(¬ ei ) ∨ 3(ei ∧ 3ri )モデル検証ツール [6] [7] を使って図.1 の作業手順

iﬀ σ |= 2(¬ ei ) or σ |= 3(ei ∧ 3ri )3(ei ∧ 3ri ) が成り立つ場合，ei と 3ri が成り立つに人為的欠陥を埋め込んで耐性を検査する．図.1 のsi が存在する．すべての ri が sj で成り立つとし∧て，σ sj .. |= ( i ri ) ∧ 3ϕ を仮定する．ここで j ≥ iするタスクである．この場合，患者を取り違えない．そのとき ϕ が真となる状態 sk が存在する．そこ
で， σ |= (ei  ri ) ⇒ 3ϕ となる．もし全てのエラー
状態 ei で σ |= (ei  ri ) ⇒ 3ϕ になるとすれば，∧σ |= i (ei  ri ) ⇒ 3ϕ となる．
もう一方の ¬ei が常に成り立つ場合について考える． 3ϕ は明らかに成り立つ．なぜならフォルトを埋め込む前の作業手順のモデルはすでに何らかの方法で検証が済んでおり，必ず全ての列でゴールに至ると仮定しているからである．

to confirm label と to compare name は誤りを発見ための重要なタスクである．そこで，この 2 つのタ
スクに 4 節で示した人為的欠陥を埋め込むことにする． H = {”confirm label”, ”compare name”} とする．図.2 はそれぞれのタスクに人為的欠陥を埋め込んだモデルを示している．この他に患者が受付番号を間違えて採血の場所に来てしまう人為的欠陥を起こすとする．その振舞をあらわすプロセス Patient が定義されている．
モデル検証するために作業手順の目的を LTL で与えなければならない．図.1 での目的は患者を取り違

表1

def

Lab =

(take sample to lab(name on receipt Lab,

患者数

作業領域

患者取り違い事故

1

—

起こらない

2

分けていない

起こる

2

分けている

起こらない

name on label Lab) : Lab)
図3

モデル検証の結果

検査室の作業モデル(Patient(”Alice”)|(P atient(”Bob”)

行わないと云った人為的欠陥が生じるとして検証した|Receipt(1, 100)場合は反例を観測できる．よって看護士に人為的欠陥|Clerk(1)を生じた場合は患者の間違いを発見しリカバリでき|T ube(1)ない可能性があると云える．
つぎに，患者には人為的欠陥は生じないとして，看|Lab(1)

護士は ”confirm label” や ”compare names” を行わ|N urse(1))
図4

ないと云った人為的欠陥が生じる検証を行う．患者が採血の状況

1 人だけの場合，患者が 2 人で作業スペースが別れえることなく検査室に検体を持っていくと云うことでていない場合，患者が 2 人で作業スペースが別れてある．これを看護士が検査室に検体を持って行った時いる場合である．いずれの場合も看護士は 1 人とし点でラベルの名前と受付表の名前が一致しているこている．それぞれで反例を得られるかどうかの結果とであると読み変える．いま，検査室をあらわすモデを表. 1 に示す．また，作業スペースが別れていない

ルを図.3 のように与えることにする． このとき，目場合 ”confirm label” と ”compare names” では十分

的を (1) の時相論理式であらわす．

でないことが反例から云える．このいずれかを怠った

23(name on receipt Lab = name on label Lab)
(1)

ときには患者を取り違えてしまう反例が見つかっている．

リカバリ可能性をモデル検証器 [7] で検証する．このツールは emptyness を検証するので (1) の否定を与

7 おわりにえなければならない．よって，与える論理式は作業手順の人為的欠陥に対する耐性をモデル検証

32¬(name on receipt Lab = name on label Lab)をもちいて解析する方法を提案した．人間の思考の出(2)

力としての行動に着目して人為的欠陥を分類し，そのとなる．また，この検証器はモデルのインスタンスを形式的な意味をプロセス代数で定義している．期待さ与えなければならない．インスタンスはある状況を再れる手順のモデルにこの意味をもとに人為的欠陥を現したのものになる．ここでは 2 人の患者を 1 人の埋め込んでいる．作業手順の耐性を検証するときに看護士が同時に採血する状況を再現する．例えば図.4

は，人為的欠陥が埋め込まれたモデルに対する作業のように与える．Nurse と Lab 以外の詳細はここで手順のリカバリーを定義した．手順の目的をあらわは省略する．

す時相論理式が与えられたとして，その反例が見つ最初に，患者は人為的欠陥を生じるが看護士は人為

かる時にはリカバリーができていないことを示した．

的欠陥を生じないとした場合について検証を行った．

この定理をもとにモデル検証をもちいて耐性を検査

患者が受付番号を間違えて採血にくるという人為的欠する方法を提案している．また，採血の手順に適用し陥を考えている．この場合 (2) を充たす列は発見できて有用性を示した．

なかった．看護士が期待された振舞をしている時には我々の解析はタスクを表すプロセス代数のアクショ

間違いを発見してリカバリできるであろう．しかし，ンとしての記号の列だけを扱っている． 4. 1 節で述

看護士にも ”confirm label” や ”compare names” をべたように記号の意味を考慮してはいない． FMEA

や FTA のようにタスクの意味を考慮しながら解析することはしていない．作業手順の耐性を向上するにはタスクの意味を理解し他の手法も併用して利用するべきである．また，反例の解析ではタスクの意味を十分理解したうえで解析する必要がある．
本稿は作業手順についてのべている．しかし，システムの操作に人為的欠陥を埋め込んだときのシス
テムの耐性を検証することにも利用できると考えている．

参 考 文 献[ 1 ] Avižienis, A., Laprie, J.-C., Randell, B., andLandwehr, C.: Basic Concepts and Taxonomy ofDependable and Secure Computing, IEEE Transactions on Dependable and Secure Computing,Vol. 1(2004), pp. 11–33.
[ 2 ] Bernardeschi, C., Fantechi, A., and Gnesi,S.: Model checking fault tolerant systems, Software Testing, Verification and Reliability, Vol. 12,
No. 4(2002), pp. 251–275.
[ 3 ] Gnesi, S., Lenzini, G., and Martinelli, F.: Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking, Proceedingsof the International Workshop on Software Verifi-

cation and Validation (SVV 2003), Mumbai, India,
Etalle, S., Mukhopadhyay, S., and Roychoudhury,A.(eds.), Electronic Notes in Theoretical Computer
Science, Vol. 118, Amsterdam, Elsevier, December
2003, pp. 57–70.
[ 4 ] Krishnan, P.: A semantic characterisation for
faults in replicated systems, Theoretical Computer
Science, Vol. 128, No. 1-2(1994), pp. 159 – 177.
[ 5 ] Milner, R.: Communication and concurrency,
Printice-Hall, 1989.
[ 6 ] 永藤直行: GDB とシステムモデルを用いたソース
コード検証器の開発, 情報処理学会論文誌 プログラミン
グ, Vol. 47, No. SIG 11(PRO30)(2006), pp. 1–12.
[ 7 ] PRESYSTEMS Inc.: A Model Checker: nhk.
http://www4.ocn.ne.jp/~presys/index_en.html.
[ 8 ] Reason, J.: Human Error, Cambridge University Press, 1990.
[ 9 ] Rushby, J.: Formal Specification and Verification of a Fault-Masking and Transient-Recovery
Model for Digital Flight-Control Systems, In Second
International Symposium on Formal Techniques inReal Time and Fault Tolerant Systems, Springer
Verlag, 1991, pp. 237–257.
[10] Swain, A. D. and Guttmann, H. E.: HANDBOOK OF HUMAN RELIABILITY ANALYSIS WITH EMPHASIS ON NUCLEAR POWER
PLANT APPLICATIONS, Draft Report NUREG/
CR-1278, U.S. Nuclear Regulatory Commission Office of Nuclear Regulatory Research, Washington,
DC, May 1982.