私は大学でHoare Logicを垣間見ました。私たちがしたことは実にシンプルです。while私が行ったことのほとんどは、ループ、ifステートメント、および一連の命令で構成される単純なプログラムの正しさを証明することでしたが、それ以上のものはありませんでした。これらの方法は非常に便利です。
フォーマルメソッドは業界で広く使用されていますか?
これらの方法は、ミッションクリティカルなソフトウェアを証明するために使用されていますか?
質問する
1779 次
10 に答える
14
サー トニー ホーアは、約 10 年前に Microsoft Research に参加しました。彼が始めたことの 1 つは、Windows NT カーネルの正式な検証でした。実際、これが Windows Vista のリリースが遅れた理由の 1 つです。Vista 以降では、カーネルの大部分が実際に wrt で正式に検証されています。デッドロックの不在、情報漏洩の不在などの特定のプロパティに。
これは確かに一般的ではありませんが、その影響という点では、おそらく正式なプログラム検証の最も重要なアプリケーションの 1 つです (結局のところ、ほぼすべての人間が何らかの形で Windows を実行しているコンピューターの影響を受けています)。
于 2009-07-28T21:32:49.023 に答える
12
これは私の心の奥底にある質問です (私は形式論理を使用したソフトウェア検証の研究者です)、これらの手法には有用な場所があり、まだ十分に使用されていないと私が言ったとしても、おそらく驚かないでしょう。業界。
「正式な方法」には多くのレベルがあるため、(たとえば、6 シグマ スタイルのプロセスに従うのではなく) 厳密な数学的基礎に基づくものを意味していると思います。いくつかの型の正式メソッドは大きな成功を収めています。型システムはその一例です。データ フロー分析に基づく静的分析ツールも人気があり、モデル チェックはハードウェア設計のほとんどどこにでもあります。また、Pi-Calculus や CCS などの計算モデルは、並行性のための実用的な言語設計に実際の変化をもたらしているようです。終了分析は、最近よく取り上げられているものです。Microsoft の SDV プロジェクトと Byron Cook の研究は、形式的手法における研究と実践のクロスオーバーの最近の例です。
Hoare Reasoning は、これまでのところ、業界に大きく浸透していません。これには、私が挙げることができるよりも多くの理由がありますが、実際のプログラムの仕様を記述して証明することの複雑さが主な原因であると思われます (それらは大きくなり、失敗する傾向があります)。多くの現実世界の環境のプロパティを表現するため)。このタイプの推論のさまざまなサブフィールドが、現在、これらの問題に大きく食い込んでいます。分離ロジックはその 1 つです。
これは部分的に進行中の (ハード) 研究の性質です。しかし、私たち理論家は、私たちの技術がなぜ有用なのか、業界のニーズに合わせて維持し、ソフトウェア開発者にとって親しみやすいものにするために、業界を教育することに完全に失敗したことを告白しなければなりません。あるレベルでは、それは私たちの問題ではありません. また、開発されている技術は、大規模なシステムで使用するには初期段階にすぎないことがよくあります。私たちは、小さなプログラムや単純化されたシステムに取り組み、数学を機能させ、次に進みます。私はこれらの言い訳をあまり受け入れません - 私たちは自分たちのアイデアを推進し、業界と私たちの仕事の間のフィードバックループを得ることにもっと積極的であるべきです (私が研究に戻った主な理由の 1 つです)。
私のウェブログを復活させて、この件に関する記事をもう少し書くのは、おそらく私にとって良い考えです...
于 2009-07-28T22:02:52.907 に答える
6
ミッション クリティカルなソフトウェアについてはあまりコメントできませんが、アビオニクス業界ではソフトウェアを検証するために、Hoare スタイルの方法を含むさまざまな手法が使用されていることは知っています。
Edsger Dijkstra のような初期の提唱者が形式的な手法はあらゆる場所で使用されるべきだと主張したため、形式的な手法は損なわれてきました。形式主義もソフトウェアサポートも、仕事に十分ではありませんでした。より賢明な支持者は、これらの方法は難しい問題に使用すべきだと考えています。業界で広く使用されているわけではありませんが、採用は増加しています。おそらく最大の進歩は、ソフトウェアの安全性をチェックするための正式な方法の使用にあります。私のお気に入りの例のいくつかは、SPINモデル チェッカーと、George Necula の証明を含むコードです。
Microsoft のSingularityオペレーティング システム プロジェクトは、実践から離れて研究に移行し、正式な方法を使用して、通常はハードウェア サポートを必要とする安全性の保証を提供することを目的としています。これにより、パフォーマンスが高速になり、保証が強化されます。たとえば、特異点で、サードパーティのデバイス ドライバーがシステムに許可されている場合 (基本的な検証条件が証明されていることを意味します)、その OS 全体をダウンさせることは不可能であることが証明されています。自分のデバイス。
正式な方法は、業界ではまだ広く使用されていませんが、20 年前よりも広く使用されており、20 年後もさらに広く使用されるでしょう。だからあなたは将来保証されています:-)
于 2009-07-28T23:47:47.907 に答える
5
はい、使用されていますが、すべての分野で広く使用されているわけではありません。hoare ロジックだけでなく、より多くのメソッドがあり、特定のタスクへの適合性に応じて、より多く使用されるものもあれば、使用されないものもあります。よくある問題は、ソフトウェアが非常に複雑であり、そのすべてが正しいことを確認することは依然として難しすぎるということです。
たとえば、定理証明器 (人間がプログラムの正しさを証明するのを支援するソフトウェア) ACL2 は、特定の浮動小数点処理ユニットに特定の種類のバグがないことを証明するために使用されています。これは大きな作業だったので、この手法はあまり一般的ではありません。
モデル チェックは、別の種類の正式な検証であり、最近ではかなり広く使用されています。たとえば、Microsoft はドライバー開発キットで一種のモデル チェッカーを提供しており、一連の一般的なバグについてドライバーを検証するために使用できます。モデル チェッカーは、ハードウェア回路の検証にもよく使用されます。
厳密なテストは、正式な検証とも考えることができます。プログラムのどのパスをテストする必要があるかなど、正式な仕様がいくつかあります。
于 2009-07-28T21:33:08.647 に答える
3
「形式的な方法は業界で使用されていますか?」
はい。
assert多くのプログラミング言語のステートメントは、プログラムを検証するための形式的な方法に関連しています。
「フォーマルメソッドは産業界で広く使われていますか？」
いいえ。
「これらの方法は、ミッション クリティカルなソフトウェアを証明するために使用されますか?」
時々。多くの場合、ソフトウェアが安全であることを証明するために使用されます。より正式には、ソフトウェアに関する特定のセキュリティ関連のアサーションを証明するために使用されます。
于 2009-07-28T21:24:37.650 に答える
2
于 2009-08-03T22:08:48.197 に答える
2
私の専門分野は、ソフトウェアに実行時エラーがないことを示すための静的コード分析の形式的手法の使用です。これは、「抽象解釈」と呼ばれる正式な手法を使用して実装されます。この手法により、基本的に as/w プログラムの特定の属性を証明できます。たとえば、a+b がオーバーフローしないこと、または x/(xy) がゼロ除算にならないことを証明します。この手法を使用する静的解析ツールの例として、Polyspace があります。
あなたの質問に関して：「形式的方法は業界で広く使用されていますか？」そして「これらの方法は、ミッションクリティカルなソフトウェアを証明するために使用されていますか?」
答えはイエスです。この意見は、自動車の電子スロットル、列車のブレーキ システム、ジェット エンジン コントローラー、薬物送達注入ポンプ、これらの業界は、実際にこれらのタイプの形式手法ツールを使用しています。
これらの業界セグメントのすべてがこれらのツールを 100% 使用しているとは思いませんが、使用は増加しています。私の意見では、航空宇宙産業と自動車産業がリードしており、医療機器産業が急速に使用を拡大しています。
于 2011-08-19T18:08:57.780 に答える
1
Polyspaceは、プログラム検証に基づくaa（非常に高価ですが、非常に優れた）商用製品です。これはかなり実用的であり、「おそらくいくつかのバグを見つける拡張ユニットテスト」から「これらの10個のファイルに欠陥がないことを示すためにあなたの人生の次の3年間が費やされる」にスケールアップします。
これは、肯定的な検証（「このプログラムは、これらの50ページの方程式が言うことを正確に実行する」）ではなく、否定的な検証（「このプログラムはスタックを破壊しない」）に基づいています。
于 2009-07-28T22:52:14.197 に答える
0
他のより手続き的なアプローチに加えて、Hoare ロジックは、Eiffel で Bertrand Meyer によってオブジェクト指向手法として導入されたDesign by Contractの基礎にありました ( Meyer の 1992 年の記事、 4 ページを参照)。Design by Contract は正式な検証方法と同じではありませんが (たとえば、DbC はソフトウェアが実行されるまで何も証明しません)、より実用的な使用法を提供すると考えています。
于 2009-10-27T10:44:16.163 に答える