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

FMEA とモデル検査を組合せた高信頼設計プロセスの提案
若林 昇

吉岡 信和

近年，様々な機器がネットワーク連携してシステムを形成している．特にシステムの構成要素ならびに構成要素間の関係が運用環境によって異なるようなオープンシステムが普及しようとしている．このようなシステムでは，運用時の振舞いを完全に予測することは困難であり，想定できていなかった重大な障害を引き起こし重大事故に陥る可能性がある．
本論文では，重大事故につながるシステムの脆弱性を発見する手法として，障害を事前に想定し信頼性を確保す
る FMEA と，システムの状態を網羅的に検証するモデル検査を組合せ，重大事故となる結果から脆弱性の原因を自動的に追求するアルゴリズムを使った高信頼設計プロセスを提案する．

Recently various information systems are connected through a network and become the huge information
system group that provides a service. Especially open systems are going to spread, in which components ofthe system and the relationship with the components change by operation environments. In such a systemgroup, it is diﬃcult to completely predict the behavior of the system, there is possibility that an unpredictedserious failure causes a serious accident. This paper proposes a high reliable design process that combinesmodel checking that can verify cyclopedically with FMEA by which we can assume faults in advance andprovide reliability.

• 不完全さ1 はじめに要求に対して仕様が完全ではなく，また，仕様に近年，ネットワークを介し，様々な情報システム同対して実装が完全ではなく，出荷時や運用時のシ士が直接あるいは間接的に接続され巨大な情報シス

ステムの振舞いを完全に把握することが困難でテム群となってサービス提供されている．このようなあることサービスでは，運用開始後にシステムの仕様が変わっ• 不確実さたり，OSS（Open Source Software）のようなブラッ事業者や利用者の要求やシステム環境がライフクボックス部品を用いたりすることが多い．

サイクルを通して変化し，設計時や運用時に機能

このようなシステムでは，下記に示す「不完全さ」

や挙動を完全に予測できないこと「不確実さ」 [3] により，出荷時や運用時のシステムのこのようなシステムにおいても，想定できていなかっ振舞いを完全に予測することは困難であり，当初想定た重大な障害に至る故障を検出し対策することで，信できていなかった重大な障害が起こる可能性がある．

頼性を高める高信頼設計プロセスを研究することを目的とする．
重大な障害に至る故障を引き起こすあらゆる原因をSuggestion of the high reliable design process thatcombined model checking with FMEA
Noboru Wakabayashi, (株) 日 立 製 作 所 横 浜 研 究 所,
Yokohama Research Laboratory, Hitachi,Ltd..
Nobukazu Yoshioka, 国 立 情 報 学 研 究 所 GRACE
セ ン タ ー, GRACE Center, National Institute ofInformatics.

検出することは一般的に難しい．障害を事前に想定し信頼性を確保するリスク分析手法として FMEA（Fail-ure Mode and Eﬀect Analysis）があるが，FMEAをソフトウェアに適用する際には，「故障モードの妥当性を検証することの困難さ」「原因を解析することの困難さ」「対策案が効果的であるのかを評価することの困難さ」があり，これらの困難さを解決する必要がある．
これらの困難さを解決する方法として，網羅的に検証するモデル検査を組み合わせて FMEA を実施する研究が広くなされている [1] [2] [5]．これらの研究では，主に故障が問題となる障害に至るかを自動的に検図1

HEMS 構成と課題出する手段としてモデル検査を用いており，反例が得られれば当該故障が問題となる障害に至ると判断しることは難しいと言える．ている．しかし，得られた反例を FMEA の表，特にオープンシステムの例の一つとして HEMS が挙げ「発生度」や「検出難易度」に反映する部分は熟年のられる．HEMS は家庭内の機器をネットワークでつ知見者に委ねられている．本論文では，これらの課題

なぎ， 電力管理，自動制御するシステムである [4]．

を解決するために，網羅的に検証するモデル検査を

図 1 に示す通り，HEMS においても上記と同様の課FMEA と組合せて，事前に想定できていなかった重題が当てはまる．例えば，運用中の個々の機器の故障

大な障害に至る故障を検出し，得られた反例から「発（ハードウェアの故障，或いは，複雑なソフトウェア生度」及び「検出難易度」を解析するガイドラインをから起因する故障），新たな機器の追加による当初想提案する．

定していなかった挙動，他社製品との連携不完全など

2 章で従来手法とその課題について述べ，3 章で従により，間違ったデータがコントローラに送信され，来手法の課題を解決する提案手法について述べ，4 章

電力管理が不適切になり，停電を引き起こしてしまうで提案手法を HEMS（Home Energy Managementといったことが起こり得る．

System）に適用した結果について述べる．5 章で関連研究について述べ，最後に 6 章でまとめを述べる.

2. 2 従来のリスク分析手法
事前に障害を分析する手法としてリスク分析手法が2 従来手法と課題ある．リスク分析手法の代表的なものに FTA（Fault

2. 1 オープンシステムにおける信頼性上の課題

Tree Analysis）及び FMEA（Failure Mode and Ef-システムの「不完全さ」「不確実さ」により，出荷

fect Analysis）がある．FTA は障害など望ましくな時や運用時のシステムの振舞いを完全に予測することい事象（トップ事象）を設定し，その要因を探るトッは困難であり，事前に重大な障害に至る故障を引き起プダウンによる分析であるが，分析は人手によりなさこすあらゆる原因を検出することは難しい．例えば，れるため，列挙された故障要因は気が付いた要因だ

このようなシステムではソフトウェアの規模が大きけになりやすく，気が付かない要因は漏れてしまう恐

く，多くのソフトウェアモジュールの複雑な組合せかれがある．例えば，トップ事象に関係しない下位部品ら作られており，モジュールごとに開発される．このが，複雑に影響し障害を引き起こすことも考えられ，ような開発では，他のモジュールの仕様を完全に把握

この場合，FTA では検出できない．すなわち，重大することが難しい．また運用中に新たなモジュールがな障害に至る故障を引き起こすあらゆる原因を検出システムに追加されることもある．このような場合，することは難しい．

新たなモジュールが当初想定していなかった動作を行

一方，FMEA はシステムを構成する部品を抽出し，う，或いは，何らかの原因でモジュールが故障し，当各部品で起こり得る障害の要因（故障モード）を列挙

初想定していなかった動作を行い，システム全体がダし，上位機能に及ぼす影響を検討するボトムアップにウンしてしまうことがある．このような重大な障害による分析であるため，検討漏れが起こりにくい．その至る故障を引き起こすあらゆる原因を，事前に検出すため，重大な障害に至る故障を引き起こすあらゆる原因を検出しやすい手法だと言える．そこで本研究では，設計工程でリスク分析手法である FMEA を用いることが有効であると判断し，FMEA を用いることにする．

2. 3 FMEA のソフトウェア適用における課題
2. 2 節で述べた通り，重大な障害に至る故障を引き起こすあらゆる原因を検出しやすい手法である

FMEA を用いることは，オープンシステムの信頼性を向上する上で有効である．
しかし，FMEA はハードウェアに対する分析手法として考案されたものであり，大規模なソフトウェアに適用する場合は，大規模ソフトウェアが持つ複雑性などにより故障モードを抽出しにくいといった課題がある．以下，FMEA の一般的な手順を示し，ソフトウェア適用における課題を挙げる．
図 2 に FMEA の一般的な手順を示す．
まずシステムを構成する要素（部品）を抽出し，各要素に対して故障モードを列挙していく．この際，前述したように大規模ソフトウェアが持つ複雑性などにより故障モードを列挙することが難しく，列挙できたとしても，列挙した故障モードが重大な影響を及ぼす

図2

FMEA の手順障害に至らない場合もあるが，故障から障害に至るパスが複雑で長いことがあり，その故障モードが重大なウェア適用においては，対策案が効果的であるのか評影響を及ぼす障害に至るか判断することが難しい．

価することは難しい．なぜなら，新たな故障を引き起故障モードが列挙できると，その故障モードの影こす可能性もあるからである．

響解析及び原因解析を行うが，ソフトウェアの場合，上記の課題をまとめると下記になる．

その原因は複雑かつ多様であり，故障から障害に至る（課題 1） 故障モードが重大な影響を及ぼす障害にパスが長いことがあり，原因を解析することは難しいという課題がある．
その後，その故障モードがどれくらいの発生頻度であるのかと，故障モードの検出難易度を解析する．
しかし，これら発生頻度及び検出難易度を解析することは熟年の知見者に委ねられることが多く，一般的に解析することは難しいという課題がある．

至るか判断することが難しい（課題 2） 故障モードから障害に至るパスが長いことがあり，原因解析が難しい（課題 3） 発生頻度及び検出難易度を解析することは難しい（課題 4） 対策案が効果的であるのかの評価が難しい

その後，影響度，発生度，検出難易度から危険度をこれらの課題を解決する方法として，網羅的に検証す評価し，対策案の検討を行う．なお，一般的には危険るモデル検査を組み合わせて FMEA を実施する研究度の高い故障モードから対策していく．

が広くなされているが，特に課題 3 については，熟対策案が決まれば，対策案を評価し，効果的な対策だと評価されれば，対策案を実施する．なお，ソフト年の知見者に委ねられており，未解決である．

更に対策案の評価では，対策案をモデルに反映さ3 FMEA とモデル検査を組み合わせた提案

せ，再度モデル検査で検証することにより，仮に新た手法な故障を引き起こしたとしても，新たな故障も検出す

3. 1 概要

ることができる．すなわち，対策案が効果的であるの

FMEA をソフトウェアに適用する際の課題を解決か評価することが難しいという課題（課題 4）を解決するために，網羅的に検証し，反例による解析が可能できることが期待できる．

なモデル検査を組み合わせた設計プロセス及び，モデル検査によって得られた反例を FMEA に反映するガ

3. 2 詳細プロセス及びガイドライン

イドラインを提案する．

以下，提案する FMEA とモデル検査を組み合わせ

2. 2 節で述べた通り，FMEA は重大な障害に至るた設計プロセスについて説明する．

故障を引き起こすあらゆる原因を検出しやすい手法

図 3 に提案する設計プロセスを示す．図 3 で示すであるが，大規模なソフトウェアに適用するのは，大提案プロセスは，図 2 で示した FMEA の手順にモデ

規模ソフトウェアの複雑性などにより故障モードを抽

ル検査のプロセスを加え，順番も少し変更したもので出しにくいなどといった課題がある．

ある．

一方，システムをモデル化し，そのシステムが持つまずシステム構成要素を抽出しモデル化する．なべき性質（＝仕様）を満たしているかを，網羅的に検お，ソフトウェアの設計が既に UML（Unified Model査するモデル検査がある．モデル検査は，システムをLanguage）などを用いたモデル設計がされている場

モデル化し，要求が満たされることを取り得る全状態合は，この手順を省くことができる．

について網羅的に検査する手法である．通常，モデル次に，重大な影響を及ぼす障害を列挙する．例え化する際，システムを適切な粒度に分割しモデル化す

ば，あるネットワークシステムにおいて，全ての機器るため，そのモデルを FMEA における部品ととらえの電源が OFF になってしまうなどの障害を列挙してることができ，モデル検査との親和性が高いといえいく．この際列挙した障害は影響度が大きいという観る．また，障害の状態をモデルに追加し，その状態に点で抽出されたものであるため，障害に対する重要至るかを LTL（Linear Temporal Logic : 線形時相度を予め決めることができる．なお，どれも同程度の論理）式や assertion 等で形式的に定義することがで影響度といえるが，列挙した障害間での相対的なレき，モデル検査の網羅性を利用してあらゆる反例を検ベル付けという意味で影響度を点数付けするとよい．

出することができる．この反例の有無から，故障モーなお，この部分は新規となる．

ドが重大な障害の状態に至るのかが判別できるので，次に，故障モードを列挙する．故障モードの列挙で故障モードが重大な影響を及ぼす障害に至るか判断は，特に「タイミング」「データ送受信」などのキーすることが難しいといった課題（課題 1）を解決できワードを基に列挙する．

ることが期待できる．

次に，前述の手順で抽出したモデル及び障害を基また，モデル検査による反例を故障としてとらえるに，モデル検査を行う．モデル検査では，「検証モデことで，原因の分析に利用できる．モデル検査では，ルの設計」「検証モデルの実装」「検証式の作成」「検故障モードから障害に至るパスを反例として定義で証」といった基本的なモデル検査の手順に従って検証きるため，原因を解析することが難しいという課題していく．

（課題 2）を解決できることが期待できる．
また，モデル検査による反例を FMEA に反映する
ガイドラインを示すことで，発生頻度及び検出難易度を解析することは難しいという課題（課題 3）を解決できることが期待できる．

「検証モデルの設計」では，下記を行う．

• 障害の状態を作成し，モデルに追加する• 「タイミング」「データ送受信」などのキーワードを基に列挙した故障モードをモデルに反映する
なお，障害の状態をモデルに追加する際は，オブザー

から，通常検出しにくいパスなのかの検出難易度を点数付けする．
ここで，モデル検査により検出された反例からこれらの発生度及び検出難易度の点数付けを行うガイド
ラインを以下に示す．
発生度に対するガイドライン
問題発生箇所の状態が起こる頻度を考慮• 機器の初期状態などの場合は頻度低いとし発生度を低くする• 該当状態が反例パス内で繰り返し通っている場合頻度高いとし，発生度を高くする
検出難易度に対するガイドライン
反例パスの経路情報から判定• パスが長い場合は，検出難易度を高くする• 通信回数が多い場合は，検出難易度を高くする
次に，これらの影響度，発生度，検出難易度より危険度の計算を行う．これにより複数ある故障モードより，危険度の高いものから対策を考えていくことができる．
まず，危険度の高い故障モードの原因解析を行う．
原因の解析ではモデル検査の結果である反例を用いて解析を行う．これにより，原因の解析がやりやすく
図3

提案プロセスなる．解析した原因の対策を検討し，対策案の評価を行う．この際，対策案をモデルに反映させ，再度モデバで実現しても良いし，assertion を追加して実現しル検査で検証することにより，仮に新たな故障を引きても良い．

起こしたとしても，新たな故障も検出できるように「検証式の作成」では，上記の障害の状態に至らないことを LTL 式で記述する．
「検証」では，イベント／アクションを故意に変えることで,なる．
モデル検査による再検証の結果，対策案が問題なければ，すなわち反例が検出されなければ，対策案は有効であると判断し，対策案を設計に反映する．

• 障害の状態に達成するか？
• 想定していない遷移が発生するか？
を検証する．
検証の結果，反例が検出される場合，列挙した故障モードは重大な影響を及ぼす障害に至ると判断でき,

4 提案手法の適用提案手法を検証するために HEMS をモデル化し，提案手法を適用した．提供した対象 HEMS システムと結果について説明する．

前述した影響度の点数付けを行う。
次に，モデル検査で検出された反例に至るパスを

4. 1 対象 HEMS システム解析し，そのパスが普段ありえるパスなのかを解析

HEMS で提供するサービスとして，コントローラし，発生度の点数付けを行う．同時に，解析したパスからの家電製品制御が挙げられる．今回は，指定した

図4

HEMS 構成概要
図5

HEMS コントローラモデル

時刻になるとコントローラからエアコンが起動される機能を例にして適用検討した．以下に今回対象とす
る HEMS システムの概要を説明する．

HEMS 内機器（図 4）
HEMS コ ン ト ロ ー ラ，エ ア コ ン ，テ レ ビ ，ブレーカ
サービス仕様• 各機器（エアコン，TV）は一定周期で自身の消費電流をコントローラに通知• ある時刻になると，コントローラは宅内の総使用電流を勘案して，エアコン起動• ブレーカは宅内の総配線電流が宅内許容電

図6

エアコンモデル流を超えた場合に OFF の状態になる識し，コントローラに通知する消費電流の観点から、

4. 2 適用結果
3 章で示した提案プロセスを 4. 1 節の HEMS シス

下記故障故障モードを列挙した．

• TV 側の消費電流通知に誤りがある

テムへ適用した．以下，図 3 に示したプロセスに従っ• エアコン側の消費電流通知に誤りがあるて適用した結果を説明する．

• コントローラからのエアコン起動コマンドに誤「システム構成の要素の抽出（モデル化）」ではりがある

HEMS システムを抽象化して状態遷移図にてモデル

上記のうち今回は「TV 側の消費電流通知に誤りが化を行った．各機器についてのモデルを図 5 から図 8ある」という故障モードについて，「ブレーカが OFFに示す．になり，全機器の電源が落ちてしまう」という重大な「重大な影響を及ぼす障害の列挙」としては，本来影響を及ぼす障害に至るかを検証することにした．

複数の障害を列挙すべきであるが，今回は，「ブレー「検証モデルの設計」においては，上述のモデル化

カが OFF になり，全機器の電源が落ちてしまう」とにおいて機器間のやりとりをモデル化したものを検いう障害を挙げた．なお、本障害に対する影響度は，証モデルとした．図 9 に検証モデルを示す．なお，障今回は単一の障害を対象としたので，最高点である

害の状態としてはブレーカが OFF になる状態をモデ「5」とした．
「故障モードの列挙」では，「データ送受信」を意ルに記述しており，ブレーカが OFF の状態にならないことを assertion で記述して検証した．

図9
図7

検証モデル

ブレーカモデル「反例とガイドラインによる発生度の点数付け」では，反例のパスにより，提案ガイドラインに従って発生しやすさを検討した．今回の例ではエアコンの起動時という初期状態のみに起こり得るので，頻度低いとし，5 段階中 2 とした．
「反例とガイドラインによる検出難易度の点数付け」では，同様に反例のパスにより，提案ガイドラインに従って検出しにくさを検討した．今回の例では反例のステップ数が 66 ステップであり今回適用した
図8

TV モデルHEMS の規模では中程度のステップ数と判断できるので，中程度の検出しにくさと設定し，検出難易度を「検証モデルの実装」では，設計した検証モデルに5 段階中 2 とした．

従って Promela を用いて作成した．なお，故障モー「危険度（致命度）の評価」では，影響度と発生度ドを検証モデルに反映させるために，コントローラに及び検出難易度を掛け算し，20 点と点数付けした．

通知する消費電流を故意に変えるような Promela 記「反例解析による故障モードの原因解析」では，反述にした．

例を解析することで，原因を解析した．今回の例で「検証式の作成」では，前述した通り，ブレーカがは，反例を解析することで，TV からコントローラにOFF の状態にならないことを assertion で記述した．

通知する消費電流値とブレーカが参照する配線電流「検証」では，作成した Promela で assertion が出値が異なっており，コントローラに通知する消費電流ないかを SPIN で検査した．

値が配線電流値より小さい値だったことが原因だと容検査の結果，assertion が成立する反例が見つかっ易にわかった．すなわち，コントローラが総消費電流た．なお，反例のステップ数は 66 ステップであった．

値でしかエアコン起動の判断をしておらず，データのこれにより「TV 側の消費電流通知に誤りがある」と誤りを検出していないことが原因であることが容易

いう故障モードは「ブレーカが OFF になり，全機器にわかった．の電源が落ちてしまう」という重大な影響を及ぼす障害に至ることが確認できた．
「影響度の点数付け」では，今回の故障モードについては重大な影響を及ぼす障害に至ることが確認できたため，影響度を前述の 5 とした．

なお，上記の手順を繰り返し，他の故障モードについても同様の手順を繰り返し，危険度の高い故障モードから対策していくが，今回は他の故障モードについては検証を省略した．
「対策案の検討」では，反例解析の結果，コントローラが総消費電流値でしかエアコン起動の判断を定義できるため，反例解析を行うことで原因を解しておらず，データの誤りを検出していないことが原析することが容易であった．例えば，今回得られ因であるとわかったので，コントローラでも配線電流た反例の各ステップにおける各変数値の変移をみ値を把握し，誤りがない場合にのみエアコンを起動することで，ブレーカが OFF になるという障害にるという対策をすることにした．

至る原因が，コントローラでは総消費電流値で「対策案の評価」では，上記対策案を検証モデルにしかエアコン起動の判断をしておらず，データの追加し，再度モデル検査にて検証した．モデル検査の誤りを検出していないことであったいうことが，結果，assertion エラーは出ず，すなわち「TV 側の容易に見つけることができた．

消費電流通知に誤りがある」という故障モードが発生

ただし，今回の例では反例を容易に解析できしても，「ブレーカが OFF になり，全機器の電源が落たが，パスが更に長い場合など，反例解析自身がちてしまう」という重大な影響を及ぼす障害にはなら

難しい場合は原因の解析も困難になると想定でないことが確認でき，対策案の有効性を確認することきる．しかし，モデル検査の反例解析についてはができた．

様々な支援ツールの研究開発がなされており，そ「対策案の実施」では，対策案を設計に反映して機器を実装するが，提案プロセスの効果に対しては無関係であるので，今回の報告では割愛した．

れらを用いることで問題解決できると考える．
課題 3 に対する有効性：
得られた反例と提案したガイドラインにより，発生頻度及び検出難易度を決めることは容易で

4. 3 結果の検討
4. 2 節で述べた提案手法の適用結果から，2. 3 節であった．
課題 4 に対する有効性：

述べた下記 FMEA のソフトウェア適用におけるそれ対策案をモデルに反映させ，再度モデル検査ぞれの課題に対して提案手法の有効性を検討する．

で検証することにより，assertion エラーが出ず，（課題 1） 故障モードが重大な影響を及ぼす障害に至るか判断することが難しい（課題 2） 故障モードから障害に至るパスが長いこ対策案の有効性を確認することができた．
以上より，適用事例に対して，本提案手法の有効性が概ね確認できた．とがあり，原因解析が難しい（課題 3） 発生頻度及び検出難易度を解析することは難しい（課題 4） 対策案が効果的であるのかの評価が難
しい課題 1 に対する有効性：

5 関連研究オープンシステムのような新産業領域はまだ実績がなく，エネルギー分野（スマートグリッド/EMS）やクラウドの分野でオープンシステムとしての問題意識が出てきた段階である †1 ．今回例で挙げた HEMS

想定した故障モードが重大な影響を及ぼす障に関しても各社製品システムは販売しているが，家庭害の状態に至ることが，網羅的に状態検査するモ内電力の見える化がメインであり，電力管理して自動デル検査により確認できた．モデル検査から得ら制御するようなものまでは製品化されていない．このれた反例のステップ数は 66 ステップであり，人事からも，オープンシステムにおける信頼性向上に関手で検討した場合，容易に検証できるステップ数する研究開発はまだ発展途上であるといえる．

ではないと判断できる．なお，モデル検査にかかFMEA とモデル検査を組み合わせる手法についてる時間は数秒程度であったので，このことから提はいくつか提案されている．例えば，BehaviorTree

案手法の有効性が確認できる．
課題 2 に対する有効性：
故障モードから障害に至るパスを反例として†1 ディペ ン ダ ビ リ ティを 必 要 と す る 新 産 業 領 域,
http://www.dependable-os.net/osddeos/top contents/shinsangyou.html

とモデル検査を組み合わせて FMEA の自動化を行っから FMEA に反映するガイドラインの検討を行ってている研究 [2] や故障発生から危害達成までのシナリいく．

オを PetriNet を用いて可視化し曖昧性を低減する手法 [5] や FMEA に確率的モデル検査を加えた手法 [1]

謝辞 本研究はトップエスイーの修了制作をもとに発展させました．

がある．これらの研究では，本研究における課題 1 に対する解決策としてモデル検査を用いているが，検証

参 考 文 献モデルの設計方針などは示されておらず，またその他[1] Grunske, L., Colvin, R., and Winter, K.: Probabilistic Model-Checking Support for FMEA, Quantitative Evaluation of Systems, 2007. QEST 2007.,
IEEE, 2007, pp. 119–128.
[2] Grunske, L., Winter, K., Yatapanage, N., Zafar,S., and Lindsay, P. A.: Experience with fault injection experiments for FMEA, Softw. Pract. Exper.,No. 41(2011), pp. 1233–1258.
[3] 所眞理雄: DEOS プロジェクト White Paper Version3.0, 科学技術振興機構, 2011.
[4] 安東宣善, 松本誠一郎, 今井光洋, 小村勝人, 片岸誠:
スマートハウス実証事例と基盤技術, 日立評論 2010.10月号, 株式会社日立製作所, 10 2010.
[5] 豊嶋伊知郎, 西川武一郎: PetriNet によるシステム非正常系可視化の検討, 信学技報, 電子情報通信学会, 112008.の課題について言及されていない．

6 まとめと今後の課題
オープンシステムにおける信頼性向上を目的として，リスク分析手法である FMEA と網羅的に状態検査するモデル検査を組み合わせた高信頼設計プロセ
ス及び，モデル検査で得られた反例から FMEA に反映するガイドラインを提案し，FMEA をソフトウェア適用する際の課題を洗い出し，全ての課題解決について，提案手法は有効であることを確認した．
今後は，確率的モデル検査を用いて得られた反例