algorithm - 重要なシステムのソフトウェア保証はありますか?

Question

それをバックアップするための正当性を証明して開発されたシステムやソフトウェアはありますか? それとも、すべての重要なシステムは、積極的なコード レビューとテスト サイクルだけで開発されているのでしょうか?

Answer 1

現実の世界では、高整合性アプリケーションのコーディングには、通常、一連のQAフープを飛び越えることが含まれます。時々、これらのフープは実際にソフトウェアを正しくすることと関係があります。

米国の医療機器業界は、FDAによって規制されています。彼らは、すべてのソフトウェア開発を含む「設計」をカバーする一連の規制を公開しています。これらの規制は、基本的にステロイドに関するISO9000です。作成され、レビュー担当者によってマークアップされ、レビューコメントで更新され、上級管理職によって承認された一連のドキュメントが必要です。規制は法律に裏付けられているため、FDAは、たとえば、テストの結果を確認した後、テストの「期待される結果」を書き込むことによって、これらの記録が改ざんされていないという証拠を確認したいと考えています。したがって、完全に安全なCMシステムをロックダウンするか、すべてを紙に署名して日付を記入する必要があります（ソースコードを含む）。FDAの検査官は実際の法執行権限を持っています。彼らが適切であると判断した場合、彼らは武装した連邦保安官であなたのソースコードを検査することができます。ただし、彼らはソフトウェアの専門家ではありません。彼らの仕事は、コードの品質を判断することではなく、すべての規制に準拠していることを確認することです。

航空業界は、ステロイドのISO-9000でもあるDO-178Bに従わなければなりません。たくさんのドキュメントを作成し、それらの間のトレーサビリティを実証する必要があります。ただし、FAAがFDAと同じQAアプローチを採用しているかどうかはわかりません。

問題は、本来あるべきことを実行するソフトウェアを作成する方法を誰も本当に知らないということです。その代わりに、私たちは一種のカーゴカルトアプローチを採用しており、ソフトウェアに高品質を吹き込むことを期待して、多くのドキュメントを作成しています。確かに、高品質のソフトウェアには明確な要件と単純な論理アーキテクチャがありますが、それは「要件ドキュメント」または「アーキテクチャドキュメント」を作成することで問題が改善されるという意味ではありません。

証拠は、コードの正確性に最大の影響を与える要因は、それを作成したチームであることを示唆しています。ただし、チームに法的な制約を書き込むことはできません。したがって、代わりに、品質を義務付ける仕事をしている人々は、代わりにプロセスに制約を書く必要があります。これが同様の効果をもたらすことを漠然と望んでいます。

Answer 2

They Write The Right Stuffを参照して、彼らがスペース シャトル用のソフトウェアをどのように開発しているかについて興味深い考察をご覧ください。

抜粋：

しかし、ソフトウェアがどれだけの作業を行うかは、それを際立たせるものではありません。注目に値するのは、ソフトウェアがどれだけうまく機能するかです。このソフトウェアは決してクラッシュしません。再起動する必要はありません。このソフトウェアにはバグがありません。人間が達成したのと同じくらい完璧です。これらの統計を考慮してください: プログラムの最後の 3 つのバージョン -- それぞれ 420,000 行の長さ -- には、それぞれ 1 つのエラーしかありませんでした。このソフトウェアの最後の 11 バージョンには、合計 17 のエラーがありました。同等の複雑さの商用プログラムには、5,000 のエラーがあります。

Answer 3

はい、正しさを証明して開発されたシステムがあります。Praxis は SPARK Ada を使用して何年もこれを行ってきましたが、現在は C と Escher C Verifier を使用しています。これは万能薬ではありません。コードが仕様を満たしていることを証明したとしても、その仕様が関係するアプリケーションに適しているかどうかを確認することは通常難しいからです。

正式な証明のより広範な採用に対する障壁の 1 つは、既存の航空ソフトウェア標準 DO-178B が正式な技術に適していないことです。現在進行中の DO-178C 書き換えは、それを修正することになっています。

Answer 4

Walter Bright によるこのコラムを参照してください。基本的に、完璧なソフトウェアを作成することは事実上不可能であると主張しています。