c++ - 安全性が重要なソフトウェアのための C++ のフォーマル メソッド

Question

Cを見ると、Cはコード内で使用できる正式なメソッド（frama-c、VCC、verifast）を適切にサポートしています。私が知る限り、C++には匹敵するものはないようです。

C++ で書かれたセーフティ クリティカルなソフトウェアを推論するために利用できる形式的な方法は何ですか?

Answer 1

私が一緒に働いている医療会社は、CoverityとKlocworkを使用して、リソース リークや初期化されていないポインターの使用などの潜在的な問題がないかコードをチェックしています。

ただし、これらはツールであり、セーフティ クリティカル コードの標準ではありません。

私が見たのは、MISRA が C++ の標準に取り組んでいるということです。彼らは C から始めて、約 5 年前に C++ の作業を開始しました。大きな問題の 1 つは、たとえば C++ の MISRA 標準では、テンプレートを使用すべきではないと規定されていることです。これは、C++ でできることを本当に制限します。ただし、そのドキュメントを出発点として使用できます。たとえば、ソフトウェアで使用されるテンプレートを標準ライブラリとブーストに含まれるものに限定したい場合があります。

Klocwork にはMISRA C++の拡張機能があることに注意してください。

それでも、優れたコードを作成するための最良の方法の 1 つは、単体テストと統合テストでテストすることです。私は何年もの間、これが他のほとんどの方法よりも信頼性が高いことを発見しました.