問題タブ [formal-verification]

• モデル チェックを使用したアプリケーションの種類は何ですか?
• どのモデル チェック ツールを使用しましたか?
• この手法を使用した経験、特に高品質のソフトウェアを提供する上での有効性を評価した経験をどのように要約しますか?

研究の過程で、 Spinを使用する機会があり、実際のモデル チェックがどの程度行われているか、組織がそれからどれだけの価値を得ているかについて興味をそそられました。私の実務経験では、ロジックに正式な検証を適用することは (当然のことながら) 考慮されていないビジネス アプリケーションに取り組んできました。SO の人々のモデル チェックの経験と、この件に関する考えについて本当に知りたいです。モデル チェックは、ツールキットに含める必要がある、より広く使用される開発プラクティスになるのでしょうか?

コンピューター プログラムは、数学的なステートメントと同じように証明できないのはなぜですか? 数学的証明は、さらに多くの証明から構築された他の証明の上に構築され、公理に至るまでです。

コンピュータプログラムはそのような構造を持っていないようです。コンピューター プログラムを作成した場合、以前に証明された作品を使用して、プログラムの真実を示すことができるのはどうしてですか? 存在しないのでできません。さらに、プログラミングの公理とは何ですか? フィールドの非常に原子的な真実？

上記に対する良い答えはありません。しかし、ソフトウェアは科学ではなく芸術であるため、証明できないようです。ピカソであることをどのように証明しますか?

アプリケーション サーバーとオブジェクト データベースの組み合わせであるプロジェクトに取り組んでおり、現在は 1 台のマシンでのみ実行されています。少し前に、分散リレーショナル データベースについて説明している論文を読み、その論文のアイデアを自分のプロジェクトに適用する方法についていくつかのアイデアを得ました。 -何もない建築。

私の問題は、分散システムとそのプロトコルの設計経験がないことです。大学で分散システムに関する高度な CS コースを受講していません。そのため、デッドロック、飢餓、スプリットブレインなどの問題を引き起こさないプロトコルを設計できるか心配しています。

質問:分散システムの設計に関する適切な資料はどこにありますか? 分散プロトコルが正しく機能することを確認する方法には、どのようなものがありますか? 書籍、学術論文などの推薦を歓迎します。

私たちのクライアントは、ソフトウェア要件を収集するための Web ベースのリッチ インターネット アプリケーションを構築することを望んでいます。基本的には、利害関係者から要件を取得するための特定のプロセスに従う Web ベースのケース ツールです。私はプロジェクト マネージャーで、まだプロジェクトの初期段階にあります。

クライアントと開発者の両方にとってツールの要件を明確にするために、形式的な方法を使用することを考えていました。正式な方法とは、何らかの形のモデリング、おそらく数学に基づくものを意味します。Z ( http://en.wikipedia.org/wiki/Z_notation )、ステート マシン、UML 2.0 (おそらくOCLなどの拡張機能を使用)、ペトリ ネット、およびいくつかのコーディングについて読んだことがあり、検討していることもあります。契約や前後の条件などのレベルのもの。他に考慮すべきことはありますか？

開発者は経験豊富ですが、使用する形式によっては、数学を学ぶ必要がある場合があります。

このプロジェクトで形式的な方法を使用する価値があるかどうか、もしそうならどの程度の価値があるかを判断しようとしています。私は「場合による」ことを知っているので、私にとって最も役立つ答えは、はい/いいえとそれを裏付ける議論です。

あなたがこのプロジェクトに参加した場合、正式な方法を使用しますか?

フォームの JML 式がどのように評価されるかを知りたいです\old(Expression[Id])。つまり、\old(vector[value-1])式がある場合\old、「値」または単に の値を参照しますvector[value-1]。前もって感謝します！

私は大学でHoare Logicを垣間見ました。私たちがしたことは実にシンプルです。while私が行ったことのほとんどは、ループ、ifステートメント、および一連の命令で構成される単純なプログラムの正しさを証明することでしたが、それ以上のものはありませんでした。これらの方法は非常に便利です。

フォーマルメソッドは業界で広く使用されていますか?

これらの方法は、ミッションクリティカルなソフトウェアを証明するために使用されていますか?

私は情報検索に興味のあるソフトウェア開発者です。現在、私は 3 番目の検索エンジン プロジェクトに取り組んでおり、同じバグなどで何度も何度も書かれているボイラープレート コードの量に非常に不満を感じています。

基本的な検索エンジンは、次の 2 つの「レイヤー」で構成される形式言語で記述できる非常に単純な獣です。

1. 「プリミティブのレイヤー」（または公理、カーネル言語-名前の付け方がわからない）。それらは、いくつかのセット (リソースのセットとして - ファイル、Web サイト)、セット上の関係 (「サイト A がサイト B にリンクする」など)、および「リソース A へのストリームを開く」、「ストリームからレコードを読み取る」などの単純な操作で構成されます。 「N 個のストリームをマージ」、「フィールド F によるレコードのインデックス セット」など。また、「YAML 形式でストリームを保存」、「XML 形式からストリームをロード」など、多くのデータ変換があります。

2. 「アプリケーション層」 - 「新しいリソースの収集」、「収集されたリソースのクロール」、「クロールされたリソースのデータベースへのマージ」、「クロールされたリソースのインデックス作成」、「インデックスのマージ」など、検索エンジンのライフサイクルを形成するいくつかの非常に高レベルの操作など。この高レベルの操作はすべて、1 から「プリミティブ」の用語で表現できます。

このような高レベルの表現は、選択したプログラミング言語で簡単にテストでき、おそらく正式に証明され、実装 (またはコード生成) できます。

では、質問: この方法でシステムを設計する人はいますか? 形式的に、厳密に (おそらく代数/群論のレベルでも)、厳密なトップダウン アプローチで? 何を読めば学べますか?

まず第一に、これは副作用のないアルゴリズムでのみ可能ですか?

第二に、このプロセス、良い本、記事などについてどこで学べますか?

私は、基本的にブルート フォース攻撃を使用して、Web アプリケーションがクラッシュしないことをテスト/検証するという壮大な考えを持っています。

単体テストや IoC のことを始めさせないでください。これはまったく別のものです。

私がやっていること、そして私が助けを求めていることは、プログラムの状態の一部を調査するインテリジェントな徹底的な検索を作成することです。

私が持っているのは、私ができることを含む Web ページです。クリックは 1 つのことであり、テキスト入力は別のことであり、ラジオ ボタンやドロップダウン リストなどの一部の入力は特定の値に制限されています。かなり基本的なこと。最終的にイベントと値のセットが有限になり、モデル化したいのは状態の進行です。これはある意味で FSM の最適化かもしれませんが、目標は、イベントと値の任意の順列を体系的に調べて、何が起こるかを確認することです。

問題が見つかった場合、明確なテスト ケースを提示できるように、できるだけ少ない労力でそのエラーを引き起こしたいと考えています。

これは正式な検証方法に関連しており、経験のある人からの助けや洞察を求めています.

大きなテストを小さなテストに分割して、小さなテストが合格したときに大きなテストも合格することを意味するようにしたいと考えています (したがって、元の大きなテストを実行する理由はありません)。小規模なテストは通常​​、時間も労力もかからず、脆弱性も少ないため、これを行いたいと考えています。このテスト分割を堅牢な方法で実現するのに役立つテスト設計パターンまたは検証ツールがあるかどうかを知りたいです。

誰かが小さなテストのセットで何かを変更すると、小さなテストと元のテストの間の接続が失われるのではないかと心配しています。もう 1 つの懸念は、小規模なテストのセットが実際には大規模なテストをカバーしていないことです。

私が目指しているものの例：