2010/12/09

決定論的故障⇒決定論的原因故障

systematic failureを決定論的故障と呼ぶことにかなり違和感があった。ソフトにバグがあれば必ずおかしな動作をする。これが決定論的な動作で、そのような故障原因は安全ライフサイクルの様なシステマティックなアプローチで解決する。と言うことだと理解している。間違っていたら指摘してもらいたい。

日本語は原因の特徴について述べていて、英語は対処法について述べている。ここに違和感があったのだが、Webを見ていたら決定論的原因故障と訳している場合も多く、こちらであれば、「決定論的原因による故障」と解釈することで何とか納得できる。

決定論的原因とは原因箇所を論理的に絞り込めたり、それを証明することができるタイプの故障で、またそのことによって完全に取り除くことができる故障原因と定義してはどうだろうか。


例えばコンポーネントがA,B,Cとあってある機能Fが動かなくなってコンポーネン
トBをB1交換すると動く場合には、A, B, B1, Cがそれぞれ正常であるという命題とすると

¬(A∧B∧C)∧(A∧B1∧C)⇒¬B

によってBが原因であることを特定かつ証明できる。この論理式は常に真になる。取り替えてみてチャンと動けばOKと言う時の論理的根拠だ。しかし、

¬(A∧B∧C)∧(A∧B1∧C)⇒¬B1
¬(A∧B∧C)∧(A∧B1∧C)⇒¬A

では、偽になる部分があり見落としを指摘される。

ソフトの故障を確率的だ言う議論もあるが上記のような論法は成立するのでソフトの故障は決定論的だろう。キャッシュを使ったCPUにおけるソフトの実行時間は確率的と言っても良いが、それでも詳細に解析すれば場合の数が多いだけでその中のどれかに、条件を揃えることができれば確定する。条件を揃えると言うのはソフトウェアの外の話である。実際、おなじソフトをキャッシュ無しで動かせば確率的変動は取り除くことができる。で、これは取り替えてみてチャンと動くと言う論法で証明できる。

ソフトを含めたシステムで、そのシステムが正しく動いたとすれば、関連するモノ・コトの全てが正しいと言える。しかし、関連するモノ・コト全てを列挙することは不可能なので。検証可能なのは列挙できる要因だけになる。このことは、ある機能が正しいと言う命題をFとすると

F⇒A∧B∧C

と表現できる。前記の例をこの形式で書くと

(F⇒A∧B∧C)∧(F1⇒A∧B1∧C)∧¬F∧F1⇒¬B

となる。この場合、全ての場合でこの推論が成立するわけではなく、A, B, C, B1全てが正しい時が反例として検出される。すなわち、列挙できていない要因によってFが失敗した場合に対応する。ここで、FとF1はテスト結果と考えた方が良いかも知れない。

0 件のコメント:

コメントを投稿