2009-04-26

A Direct Path to Dependable Software




A Direct Path to Dependable Softwareの要点を途中までメモってみました。

[注意]
1. 意訳+要約のため、かなり端折っている。
2. 微妙に意味の解釈が間違っている部分がある気がする。

※続きはImplementationから


Review articles
A Direct Path to Dependable Software
-Who could fault an approach that offers greater credibility at reduced cost?-

Daniel Jackson

Communications of the ACM
Vol. 52 No. 4, Pages 78-88
10.1145/1498765.1498787

※Introduction
ソフトウェアの信頼性の話
ーEx. シカゴ病院の薬のデータベースにバグがあり、情報が一夜で失われた。
ーこのような事件は電子投票/航空便の制御/核パワー/エネルギー配信でも起こるのでは?

組み込みソフトウェアの普及率の上昇につれて、大きなリスクを人々にもたらす。
ー特に医療分野において、ソフトウェアは人を生かすことも殺すこともできる。
ーー例)ペースメーカーとか
ーー1985-2005年までの、医療機器の欠陥による事故数は600,000。うち死亡者は30,000
ーー医療機器の欠陥事故の少なくとも約8%は、ソフトウェアによる事故。
ーーー組み込みソフトウェアが増えれば、ソフトウェアによる欠陥事故はもっと増えるだろう。

今までは、プロセスやツール/技術などのやり方が信頼性ソフトウェアを作ると信じられていた。
ーしかし、それら信頼性の証拠を示すには、indirectなアプローチである。
ーーこの記事では、信頼性ソフトウェアである確たる証拠を示すdirectなアプローチを主張する。
ーこのアプローチの特長は、2つある。
ーー真実性の向上:やり方の効果による不慮の事故ではないという主張ができる。
ーーコストの削減:開発資源を”最も重要な部分”に焦点を当てて、開発できる。
ーーー必要十分な開発資源で開発ができるため、冗長なコストを削減できるということ。

[The Need for a Direct Approach]
Dependable System:人々が信頼することができるシステム
ー理性的な人/組織にとって、利益がリスクを上回るような証拠があるシステム
ーー証拠が無ければ、safeとは言えない

将来、突出したソフトウェア開発技術がソフトウェア品質の証拠を作り上げるかもしれない。
しかしながら、今日の技術は、そのような技術とは程遠いところに位置している。
ー今までの経験を元にソフトウェアの欠陥率を予期することは出来るが、それを0にすることはできない。

例えば、車における、組み込みソフトウェア以外の技術について考えてみる。
ーNational Highway Traffic Safety Administrationのデータベースには、
年間約40,000件の重大な事故が記録されている。研究者は、その事故データ情報を元に
どのようなデバイスが最も安全なのかを、事故情報を比較しながら研究できる。
例)結果として、シートベルトやエアーバッグが、安全な車のデバイスとして誕生。

一方で、ソフトウェアにはこのような比較できる情報が無い。
ーどのようなソフトウェアの効果が、安全をもたらしたのか、または事故原因をもたらしたのか、
見分けることは難しい。よって、ソフトウェア開発事業会社にとって、事故データベースを
使った自社システムの有用性を証明することは難しくなる。結果として、消費者の
システム購入の意思決定を強く左右するようなデータをあつめることができなくなる。

加えて、現状では、ソフトウェアによる事故データには十分の情報が備わっていないことが挙げられる。
会社は、自社の基本的な事故情報を保有しているが、政府は各会社のソフトウェア事故情報を集めたような
データベースを持っていない。結果として、ソフトウェア事故から学ぶべき一般的な教訓を得にくい現状がある。

この数十年の間、私たちはソフトウェア品質を著しく向上させる技術およびアプローチを開発してきた。
それらの技術およびアプローチとは、以下の4つを含んでいる。
1. よいプラットフォーム:安全プログラミング言語, 独立したアドレス空間のOS, 仮想マシーン
2. よいインフラの構築:configulation control, bug tracking, treacibility
3. よいプロセス:spiral/agile model, prototyping
4. よいツール:統合環境, 静的解析器, model checker
加えて、以下の5つの基盤的な技術を作り上げた。
1. 問題の構築化技術
2. デザインモデルの技術
3. Software Architectureの技術
4. 検証技術
5. テスト技術
しかしながら、これら全ての技術は誤って使われることが多く、また、成功を保証するものではない。
経験に基づくソフトウェア構築技術は、上述のギャップを埋め、科学的測定法の有用性を提供したが、
今でもなお、ソフトウェアシステムの品質の確たる証拠を、簡単に、かつ自信を持って突き詰める技術ではない。

たくさんの保証規格は、ベストプラクティスを強制するように仕向けた、
よく工夫された考案であったが、一方で、正反対の効果も持ちはじめていた。
ーベストツールの使用やソフトウェアの危険箇所に注意するように促していた代わりに、
厄介な要求を義務として課した。
ーー時代遅れで、統一的で、同じ技術を義務化した。
ーーー結果として、本当に価値があるのかよく分からない、同じような仕様書が増えた。
The Common Criteria security certification(MSがwindowsに対して取得した証書)
を取得するためにはコストがかかる。また、そのコストは、本質的なバグフィックスにかかる
コストよりも大きいため、会社に取っては有用性の低いことだと館が得られてきた。

政府は、基本的な証拠を元に、よくソフトウェアシステムを評価する立場に位置していた。
ーいくつかのプロセスに対して、いくつかのテストが任意に行われた。
ーその検証テストは時々、破滅的に失敗することがあった。
ーー例)パナマのFDA-certified radiation-therapyにおける悲劇的な事件(2001)
ーー最も効果の高いと言われている規格は高価な上に、その価値を評価することが難しい。

上述とは違うアプローチとして、"goal-based"または"case-based"検証がはやっている。
このアプローチは、従来のあるやり方を強制するというアプローチと違って、開発者が呼ばれる。
ーそこで、claimed dependability goalsを満たすシステムだという直接的な証拠を提供する。
ーーU.K., Ministry of Defenceはこのアプローチで、規格獲得プロセスを著しく簡単化した。

この直接的なアプローチは、アメリカの証明機関や規格付与機関において未だ採用されていない。
最近、いくつかの政府機関では、現状のアプローチのコストと効果について見直している。
ーこの研究によって推奨されているアプローチこそ、本記事の根幹を成すものである。


[Why Testing Isn't Good Enough]
ソフトウェア開発者のレパートリーの中で、テストとは決定的なツールである。
そして、自動化されたテストを行うことは、一つの技術的能力があることの印である。
ー例)欠陥を見つけるためのRegression Test
どんどんと増えていく広大なテスト領域を覆う唯一の方法は、機械の力を使うことである。
ー多くの研究者がこれを認めるようになってきている。
Edsger Dijkstraによる以下の提言がある一方で、
ー"testing can be used to show the presence of errors but not their absence"
テストすることが信頼性を証明する十分な証拠になる、と信じている人たちが増えている。

私たちがテストに対して知っている経験は、この信条は間違っていることを指摘している。
ー小さいソフトウェアなら徹底的にテストできるが、一般的なソフトウェアは広大過ぎて
全てを徹底的にテストすることは難しい。
ーーソフトウェアを起動してすぐの入力と、いくつかの操作をした後の入力では意味が異なる。
ーーー全ての分岐を網羅的にテストすることは極めて難しい。

もう一方のアプローチは、テスト範囲を分散して、リスクの高いところを集中的にテストすることである。
ーしかしながら、信頼性を得られるために必要なテスト数は、想像以上に膨大である。
ー例)1,000の入力に対して99%の信頼を得るためには5,000のテストが必要。
5,000のテスト中でバグを10個発見したら、20,000テストが追加で必要になる。
ーー故に、バグの発見は自信の向上にはつながらない。

このような状況下では、テストでバグを発見すると、
さらに高いレベルでのテストが要求されるため、
テストにかかるコストはねずみ算式に膨れ上がる。

それにも関わらず、現存の証明方法の多くは、未だにテストに依存している。
ー自信でシステムを保証するためには"five nines"信頼性を達成する必要がある。
ーー100,000時間実行し続けてもバグが起こらないシステム
ーーーこのような信頼性の保証方法はとても現実的ではない。


[A Direct Path]
信頼性を保証するための直接的なパスとは、批評を実証することである。
ー何がシステムを構成するのか、何がシステムに信頼性をもたらすのかを考える。

システムとは、ハードウェア/ソフトウェア/使用者によって成り立つ製品のこと。
ー例)飛行機同士の空中衝突はパイロットの操作によって起こすこともできる。
ーーシステムは、人為的な事故をシステムの仮定から除いたとき、
設計全体のうちの、重要な部分にのみ設計を集中することができる。

信頼できるシステムとは、ある仕事を信頼して与えられるシステムのことである。
ー信頼できるシステムとは、証拠なしには成り得ない。
ーバグのないシステムではなく、失敗が起こらないことが証明されているシステムである。

信頼性は利益とコストのトレードオフである。
ー飛行機の空路制御や核パワー、電力の配備において、社会は寛容ではない。
ーーこのような重要な部分の技術には、多大なコストを掛けて、
大規模にソフトウェア開発を行い、また、その信頼性の証明を行わなくてはならない。
危険な状態は、その使用されたときの前後関係に依存する。
ー例)放射線療法の用量を計算するために、スプレッドシートのマクロ関数を使うことは危険
ー携帯のネットワークやGPSのようなシステムは、多くのアプリケーションによって使われているので、
そのシステムが壊れてしまったら、悲劇的な状況に陥る。

信頼性は、大規模なスケールにおいて、簡単に測定することができない。
ー多様な前後関係によって失敗は起こるので、測定を数値ではかることは難しい。
ー信頼性は、その用途によって必要十分なレベルが異なる。
ーー高い信頼性:放射線治療の用法計算、クレジットカードの数値計算
ーー低い信頼性:ネットショッピングにおいて、購入するためにストックした商品の紛失
ー高い信頼性が必要なシステムでは、機械が無断で重要な変更を行うことは許されない。

以上のことを具体化すると、以下の3つが要求される。
1. どの部品(software, physical, human)が信頼性を向上させるか決めること
2. 決定的なプロパティを確認すること
3. どのレベルの信頼性を満たすべきなのかを決定すること

[Properties and where they reside.]
決定的なプロパティは、具体的には以下の2つに分類される。
1. プロパティは個々の機能を関連付けて成り立つ
2. プロパティがいくつかの機能を横切るように使う

信頼性においては、プロパティに焦点を当てることは、個々の機能に焦点を当てるよりも効率的。
ープロパティは機能的に分類されている。また、個々の関数のまとまりの意味をもっている。
ーEx. データベースにおける決定的なプロパティ
ーーログイン時に使う関数をチェックするより、ログインの一連の流れをチェックした方が良い。

いくつかのソフトウェアシステムは、全体的な仮想サービスを提供する。
ーただし、物理的な干渉は除く。
システムの目的が物理的な現象を生成/制御/監視するようなとき、
決定的なプロパティを表現する語彙を形成しなくては成らない。
これは一見明らかに見えるが、そこにはソフトウェアへのインターフェースに関する
記述要求の長い慣習が存在する。
ー例)放射線療法のアプリケーションにおける決定的なプロパティとは以下のようなものではない。
ーー放射されるビームが有界の緊張を持つこと。
ーー正しい信号がビーム生成器に送られること。
ーービームの量の設定において、正しいコードが記述されていること。
ー放射線療法のアプリケーションにおける決定的なプロパティとは、
患者が過剰な放射線を浴びないことである。

そこには、ある終わりにおいて、システムの物理的な効果と繋がっている一連のイベントがある。
そのイベントには、ある他の終わりにおいて実行された、途中命令の周辺機器の信号がある。
決定的なプロパティが使われた現象を定式化していけばいくほど、
ユーザに対する基本的な配慮は弱まっていく。

評判の悪い事件は、ソフトウェアに近づけていくことによる、潜在的な恐ろしさを示している。
ー例)An Airbus A320 landing at Warsaw Airport in 1993

ー省略

[The dependability case. ]
信頼性に対する証拠は、ケースによって異なる。
ーそのケースに当てはまるかどうかは、開発によって異なる。
ーーしかし、ある重要な特徴がある。

1. ケースはサードパーティの証明機関によって評価される。
ー証明機関は開発者と顧客からなる独立した機関。
そのケースが正常なケースとチェックするための努力は、最小でなければ成らない。
ー信頼性できるケースは公式の証明のようなもの
ーー構成するのは難しいが、チェックするのは簡単。
評価を行う際に、システム開発や特定のアプリケーションにおける専門知識を必要としては成らない。

2. ケースは完全でなければならない。
ー決定的なプロパティの持つ主張については、ホールが一つもないということ。
ーー正当でない他のどの仮定も、ノートされる。
ーーー責任の所在をはっきりとさせるため。
ーー例)”コンパイラは正確なコードを生成する”というケースに置ける信頼性
ーー例)OSやミドルウェアは、決定的なプロパティにおいて生成されたメッセージを確実に運ぶ
ーー例)ユーザはある信頼されているプロトコルに必ず従う

3. ケースは正常でなければならない。
ー以下のようなことをすべきではない
ー例)網羅的ではないテストを元にした手続きに対して、完全な正確さを主張すること
ー例)保証されていない仮定を作ること
ー例)弱いメモリモデルの言語のプログラムにおいて、判断を下すこと???


[Implementation]
※続きはあとで。

0 件のコメント: