プログラムの検証の正式な方法は、産業界に位置していますか？
https://stackoverflow.com/questions/1196803
-
20-09-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russian質問
垣間見ることができました Hoare Logic 大学で。私たちがしたことは本当に簡単でした。私がしたことのほとんどは、で構成される単純なプログラムの正確さを証明することでした while ループ、 if ステートメント、および一連の指示、しかしそれ以上のものはありません。これらの方法は非常に便利です！
業界では正式な方法が広く使用されていますか？
これらの方法は、ミッションクリティカルなソフトウェアを証明するために使用されていますか？
解決
これは私の心に近い質問です（私は正式なロジックを使用したソフトウェア検証の研究者です）。したがって、これらの手法には有用な場所があり、まだ十分に使用されていないと言うとき、おそらく驚かないでしょう。業界。
「正式な方法」には多くのレベルがあるので、私はあなたが厳しい数学的ベースで休んでいるものを意味すると思います（たとえば、6シグマスタイルのプロセスに従うのではなく）。いくつかのタイプの正式な方法が大成功を収めています - タイプシステムは一例です。データフロー分析に基づく静的分析ツールも一般的であり、モデルチェックはハードウェア設計でほぼ遍在しており、PI-CalculusやCCなどの計算モデルは、同時性のための実際の言語設計の実際の変化を刺激しているようです。終了分析は最近多くの報道をしたものです。MicrosoftでのSDVプロジェクトとByron Cookの作業は、正式な方法での研究/実践のクロスオーバーの最近の例です。
Hoareの推論は、これまでのところ、業界に大きな侵入をしていませんでした - これは私がリストできるよりも多くの理由ですが、私はほとんどが執筆の複雑さと実際のプログラムの仕様を証明することになっていると思います（彼らは取得する傾向があります 大きい, 、そして多くの現実世界環境の特性を表現できません）。このタイプの推論におけるさまざまなサブフィールドは、現在、これらの問題に大きな侵入をしています - 分離ロジックは1つです。
これは部分的に進行中の（ハード）研究の性質です。しかし、私たちは、理論家として、私たちのテクニックがなぜ有用であるかについて、業界のニーズに関連し、ソフトウェア開発者に親しみやすくするために、業界を完全に教育することができなかったことを告白しなければなりません。あるレベルでは、それは私たちの問題ではありません - 私たちは研究者、数学者、そして実際の使用は私たちの心の中で最も重要ではありません。また、開発されている技術は、多くの場合、大規模なシステムで使用するにはあまりにも胚性です - 私たちは小さなプログラム、簡素化されたシステムに取り組み、数学を機能させ、先に進みます。私はこれらの言い訳をあまり購入しません - 私たちはアイデアを推進し、業界と仕事の間でフィードバックループを取得するのにもっと積極的に積極的に取り組むべきです（私が研究に戻った主な理由の1つ）。
おそらく、私のウェブログを復活させ、このようなものに関するいくつかの投稿を作るのは良い考えでしょう...
他のヒント
さて、Tony Hoare irは約10年前にMicrosoft Researchに参加しましたが、彼が始めたことの1つは、Windows NTカーネルの正式な検証でした。確かに、これはWindows Vistaの長い遅延の理由の1つでした。ビスタから始まる、カーネルの大部分は それは 実際に正式に検証されたWRT。デッドロックの欠如、情報の漏れの欠如などの特定のプロパティに。
これは確かに典型的なものではありませんが、おそらくその影響という点で、正式なプログラム検証の最も重要なアプリケーションです（結局、ほぼすべての人間は、ウィンドウを実行しているコンピューターによって影響を受ける形または形で何らかの形であります）。
アビオニクス業界は、Hoareスタイルの方法を含むソフトウェアを検証するためにさまざまなテクニックを使用していることを知っていますが、ミッションクリティカルなソフトウェアについてはあまりコメントすることはできません。
Edsger Dijkstraのような初期の支持者が、どこでも使用すべきだと主張したため、正式な方法が苦しんでいます。形式主義もソフトウェアのサポートも仕事に任されていませんでした。より賢明な支持者は、これらの方法は難しい問題に使用されるべきであると考えています。それらは業界で広く使用されていませんが、採用は増加しています。おそらく最大の侵入は、正式な方法を使用することでした 安全特性 ソフトウェアの。私のお気に入りの例のいくつかはです スピン モデルチェッカーとジョージネクラのプルーフキャリーコード。
練習から研究に移動すると、Microsoft's 特異点 Operating-System Projectは、通常、ハードウェアサポートが必要な安全保証を提供するために正式な方法を使用することです。これにより、パフォーマンスが高速化され、保証が強くなります。たとえば、特異点では、サードパーティのデバイスドライバーがシステムに入ることを許可されている場合（基本的な検証条件が証明されていることを意味します）、OS全体を倒すことはできないことを証明しました。独自のデバイス。
正式な方法は業界ではまだ広く使用されていませんが、20年前よりも広く使用されており、20年後はさらに広く使用されています。だからあなたは将来的に根付いています:-)
はい、それらは使用されますが、すべての分野では広くありません。 Hoare Logicだけでなく、指定されたタスクの適合性に応じて、より多く使用され、一部はより多く使用されています。一般的な問題は、SOFwareがBiiiiiiigであり、すべてが正しいことを確認することはまだ問題が大きすぎることです。
たとえば、定理プロバー（人間がプログラムの正確性を証明するのを助けるソフトウェア）ACL2は、特定のフローティングポイント処理ユニットに特定のタイプのバグがないことを証明するために使用されています。それは大きな仕事だったので、このテクニックはそれほど一般的ではありません。
別の種類の正式な検証であるモデルチェックは、今日かなり広く使用されています。たとえば、Microsoftはドライバー開発キットの一種のモデルチェッカーを提供し、共通のバグのセットのドライバーを検証するために使用できます。モデルチェッカーは、ハードウェア回路の検証にもよく使用されます。
厳密なテストは、正式な検証とも考えることができます - プログラムのパスをテストするなどの正式な仕様がいくつかあります。
「業界では正式な方法が使用されていますか？」
はい。
assert 多くのプログラミング言語のステートメントは、プログラムを検証するための正式な方法に関連しています。
「業界では正式な方法が広く使用されていますか？」
いいえ。
「これらの方法は、ミッションクリティカルなソフトウェアを証明するために使用されていますか？」
時々。より多くの場合、彼らはソフトウェアが安全であることを証明するために使用されます。より正式には、それらはソフトウェアに関する特定のセキュリティ関連の主張を証明するために使用されます。
業界では、正式な方法には2つの異なるアプローチがあります。
1つのアプローチは、開発プロセスを完全に変更することです。言及されたZ表記とBメソッドは、この最初のカテゴリにあります。 Bは、パリの無人の地下鉄線14の開発に適用されました（チャンスがある場合は、前のワゴンに登ります。目の前でレールを見る機会を得ることはあまりありません）。
もう1つのより漸進的なアプローチは、既存の開発と検証プロセスを保存し、新しい方法で一度に一度に検証タスクの1つのみを置き換えることです。これは非常に魅力的ですが、分析が簡単ではないことが多い言語を終了するための静的分析ツールを開発することを意味します（設計されていないため）。 （たとえば）に行く場合
http://dblp.uni-trier.de/db/indices/a-tree/d/delmas:david.html
（申し訳ありませんが、新しいユーザーに許可されたハイパーリンクは1つだけです:(）
Cプログラムの検証（静的分析装置Astree、Caweat、Fluctuat、Frama-C）およびバイナリコード（Absint GmbHのツールを使用）の検証に対する正式な方法の実用的なアプリケーションのインスタンスがあります。
ちなみに、上記のツールリストのHoare Logicに言及して以来、警告のみがHoare Logicに基づいています（Frama-CにはHoare Logicプラグインがあります）。その他は、より自動的なアプローチを備えた別の手法である抽象的な解釈に依存しています。
私の専門分野は、ソフトウェアに実行時間エラーがないことを示すために、静的コード分析のための正式な方法を使用することです。これは、「抽象的な解釈」が知られている正式な方法手法を使用して実装されます。この手法により、基本的にAS/Wプログラムの特定のアートビュートを証明できます。たとえば、A+Bがオーバーフローしないか、x/（xy）がゼロで除算されないことを証明します。この手法を使用する静的分析ツールの例は、PolySpaceです。
あなたの質問に関して： 「業界では正式な方法が広く使用されていますか？」 と 「これらの方法は、ミッションクリティカルなソフトウェアを証明するために使用されていますか？」
答えはイエスです。この意見は、私の経験に基づいており、自動車の電子スロットル、列車用のブレーキシステム、ジェットエンジンコントローラー、ドラッグデリバリー注入ポンプなどの安全性批判システムを制御するために埋め込みソフトウェアの使用に依存する産業向けのポリススペースツールのサポートに基づいています。など。これらの業界は、実際にこれらのタイプの正式な方法ツールを使用しています。
これらの業界セグメントの100％がすべてこれらのツールを使用しているとは考えていませんが、使用が増加しています。私の意見では、航空宇宙と自動車産業が主導し、医療機器業界が急速に使用されています。
ポリススペース プログラムの検証に基づいて、AA（恐ろしく高価ですが非常に良い）商業製品です。それはかなり実用的であり、「おそらくいくつかのバグを見つけるユニットテストの強化」から「あなたの人生の次の3年間がこれらの10のファイルがゼロの欠陥を持っていることを示すのに費やされる」から拡大するという点で拡大します。
これは、否定的な検証（「このプログラムはスタックを破壊しない」）に基づいています。代わりに肯定的な検証（「このプログラムは、これらの50ページの方程式がそうすることを正確に行います」）。
他のより手続き的なアプローチに加えて、ホアーロジックは 契約による設計, 、エッフェルのバートランド・マイヤーによってオブジェクト指向のテクニックとして導入された（1992年のマイヤーの記事をご覧ください, 、4ページ）。契約別の設計は正式な検証方法と同じではありませんが（一つにはDBCはそうではありません 証明 ソフトウェアが実行されるまで）、私の意見では、より実用的な使用を提供します。
