近年、コンピュータシステムは我々の日常生活のあらゆる面に浸透してきており、その障害はただ単に不便さをもたらすばかりではなく、人命にかかわるような極めて重大な事態を引き起こす危険性をもっている。従来、システムの障害は、構成要素の物理的な故障により引き起こされることが多かったが、最近、システムの大規模化、複雑化、高機能化が進み、設計故障がシステムの障害の最も大きな要因となってきている。ここで設計故障とはいわゆるバグのことである。こうした状況を解決するための方策として、近年、システム稼働段階において、設計故障が原因となってエラーが起こっても、システムが動作し続けられることを目的とした、設計フォールトトレランスというアプレーチが脚光を浴びている。 設計分散(design diversity)は、設計フォールトトレランスを実現するための最も広く使われている手法の1つである。設計分散は、多重系を構成する際の要素として同じ実装を用いるのではなく、同じ外部仕様をもとに複数のチームが独立に開発した、設計が異なる実装を用いる。設計分散は、ある入力に対して一部の実装で設計故障に起因したエラーが起きた場合にも、他の実装が正しい結果を出せば、システム全体としては正しい処理を続けることができる、という考え方に基づいている。現在、NASAのスペースシャトル、ボーイング777、エアバスA320といった主要民間航空機の飛行制御装置、原子力発電所の安全停止装置、そして、ATC(自動鉄道制御装置)などといった高信頼性を必要とするシステムに設計分散は広く導入されている。しかし、これまで、設計分散に対しては、適用するためにかかる膨大な開発コストに見合う程には、システムの信頼性を向上させないのではないか、という多くの批判があった。設計分散は、コスト効率が低く、その適用は膨大な開発コストを許容できるような一部のクリティカル・システムに限られるべきである、と言われてきた。 独立した開発という点に関して、設計分散の実現アプローチは次の2つに分類することができる。1つは、異なる開発チームに対して、異なる言語で記述された異なる外部仕様、異なるプログラミング言語、異なるアルゴリズム、異なるデータ形式を採用することを強制する「強制的な」設計分散である。「強制的な」設計分散はより多様な実装を開発することを目的としている。そして、もう1つはそのような制約を課さない「自然な」設計分散である。ここで注目すべきは、この「自然な」設計分散が、複数のインブリメンタが共通の外部仕様をもとに独立に実装を開発する標準化アプローチと概念的に等しいことである。例えば、TRONプロジェクトではシステム全体をアプリケーション・マンマシン階層、オペレーティングシステム階層、インストラクション・プロセッサ階層の3階層に分割し、それぞれの階層の外部仕様を定義するという標準化アプローチをとっている。現在、我々はTRONプロジェクトを基盤として、システム全体をアプリケーションプログラム、オペレーティングシステム、ハードウェアの3つの階層に分割し、それぞれの階層に1つの外部仕様を与えて設計分散を適用する多階層設計分散(Multi-Layered Design Diversity,MLDD)アーキテクチャを研究している。本研究の主な成果の1つは、標準化プロジェクトが、設計分散を実現するための有効な基盤となる得ることを示したことである。これにより、設計分散の適用可能分舒を大幅に拡大することできるようになる。 本研究の目的は、「自然な」設計分散に基づいて設計フォールトトレランスを実現する機構を設計、実装、評価することである。本研究では、MLDDアーキテクチャを提案し、本アプローチが有効となるために必要な仮定が成立することを示した。そして、その設計フォールトトレランス機能を考案し、TRONプロジェクトにおいて開発された実装を用いて実現し評価した。次に、より具体的に本研究の成果を挙げる。 MLDDアーキテクチャでは、各階層のすべての実装が同じ外部仕様を用いる。MLDDアーキテクチャが有効となるためには、1つの外部仕様を使うことが、複数の実装間に相関関係のある設計故障を生むことにつながらない、という仮定が成立する必要がある。本研究では、産業用の組み込みシステムに使用することを目的として作られたITRON2リアルタイムマルチタスクオペレーティングシステム外部仕様をもとに3つの企業が独立に開発した3つの製品のリリース後3年間において発覚した設計故障を分析することで、この仮定が成立すると期待できることを確認した。 また、本研究では、異なるオペレーティングシステムの実装同士をシステム稼働時に組み換えることで後方エラーリカパリーを提供する機構を考案した。本機構では、周期的にオペレーティングシステムのエラー検出を行い、エラーを検出した場合には、現在のオペレーティングシステムの実装を設計が異なる別の実装に組み換えて、最新のチェックポイントから再実行する。本機構は、大きく分けて、エラー検出機構、チェクポイント機構、実装間の組み換え機構の3つから構成される。 オペレーティングシステムの動作は現在のシステム内部状態に依存する。よって、新しい実装が元の実装の動作を引き継ぐためには、元の実装の内部状態を引き継ぐ必要がある。しかし、独立に開発された実装間では、内部状態の構造は異なるので、新しい実装は、元の実装の内部状態をそのままでは使用することはできない。そこで,元の実装の内部状態の構造を、標準構造を介して、新しい実装の内部状態の構造に変換するような機能を伴った実装間の組み換え機構を考案した。そして、ITRON2オペレーティングシステム外部仕様をもとに3つの企業が独立に開発したを実装を用いて実現した。この際、各実装の全体のソースコードを高々7.6%書き換えた。 実行時エラー検出テストは、先に述べた後方エラーリカパリー機構とって重要なばかりではなく、コスト制約が大きいシステムに設計フォールトトレランス機能を持たせるという点からも重要である。しかし、これまでにエラー検出テストのシステマティックな生成手法は確立されていなかった。我々は、実行時エラー検出テスト生成手法として、SBACCG(Specification-Based Consistency Checks Generation、仕様に基づいた適応化一貫性チェック生成)手法を提案した。SBACCG手法は、導出段階と適応化段階の2つの段階から構成される。導出段階では、モデル指向の形式的外仕様記述言語で記述された仕様から、一貫性テストの集合が1つ生成される。次の適応化段階では、導出段階で生成された一貫性テストが各実装の内部構造に応じて適応化される。現段階では、最も広く用いられている形式的仕様記述言語の1つであるZを採用している。本論文では、ITRON2仕様をもとに2つの企業が独立に開発したオペレーティングシステムに対してSBACCG手法を適用した例を紹介する。 我々は、考案した後方エラーリカパリー機構を2つのITRON2オペレーティングシステムの実装を用いて実現した。そして、実装した機構のエラーの潜伏(error latency)、および、エラーの伝搬(error propagation)を評価するためにフォールト・インジェクション技法を用いた実験を行った。ITRON2オペレーティングシステムの稼働段階において残存する設計故障に関する分析結果を参考にして、我々は95個の挿入する設計故障を選んだ。実験の結果、我々が提案した後方エラーリカパリー機構は、低いエラー潜伏率、および、小さいエラー伝搬を達成できることが分かった。 多くの構成要素がコスト制約をもつような我々の生活環境においては、できるだけ低いコストで提供できるフォールトトレランス機能が望まれる。本研究で提案したSBACCG手法が生成するようた、実行時エラー検出テストを使用することは、1つの有望なアプローチと考えることができる。しかし、これまで、実行時エラー検出テストがどれ程のエラー検出能力をもつのかは確認されていない。ところで、仮に、設計故障がない実装を開発することができるならば、設計フォールトトレランスは不要であろう。しかし、現段階では、このようなことは通常の実用システムには当てはまらない。実行時エラー検出テストには、テスト段階において見逃された設計故障に対応することが求められる。 開発コストや期間の点で効率良く、高い信頼性をもった設計を実現するためには、設計フォールトトレランス手法と従来の設計フォールトアボイダンス手法を補完的に採用するべきである。設計フォールトアボイダンスとは、開発段階において、できるだけ設計故障が生じないようにしたり、生じてしまった設計故障をできるだけ除去する、といったアプローチのことである。我々は、これまで、設計フォールトトレランスだけではなく、設計フォールトアボイダンスに関しても研究を行ってきた。設計フォールトアボイダンスに関しては、SBATCG(Specification-Based Adaptive Test Case Generation、仕様に基づいた適応化テストケース生成)手法を開発した。 SBATCG手法は、仕様の記述と各実装の内部構造の双方を考慮してテストケースを生成する。しかし、通常の規模をもった実際の実装の内部構造の隅々を、すべての可能な入力のもとで活性化することは現実的には難しい。このため、テスト段階で見過ごされる設計故障が生じてしまう。我々は、フォールト・インジェクション技法を用いた実験を行うことで、SBATCG手法が生成したテストケースが取り除くことができなかった設計故障を、SBACCG手法が生成したエラー検出テストが検出できることを示した。 |