問題タブ [formal-verification]

私はソフトウェアのモデルの一貫性のチェックに取り組んでいます。これを行うには、UML2.0シーケンス図の線形時相論理を作成する必要があります。体に同じツールが他にある場合は、できるだけ早く対応してください。私はあなたに非常に義務があります。私は魅力的なツールが同じためのプラグインを持っていることを発見しました。魅力的なツール（CHecking ARchitectural ModelconsistentY）のソースコードを持っている人はいますか？彼らのウェブサイトでは利用できません。

前もって感謝します。

ring0で実行されるプログラムのフォーマル検証なしでセキュリティを確保するにはどうすればよいですか？ユーザースペースのカーネルスペースを変えずにVMを使用できますか？

大学で形式的なシステムについて教わりましたが、実際には使われていないようで残念でした。

私は、テストではなく証明によって、コード (オブジェクト、関数など) が機能することを知ることができるという考えが好きです。

私たちは皆、物理工学とソフトウェア工学の間に存在しない類似点に精通していると確信しています (鉄は予測通りに動作し、ソフトウェアは何でもできます - 誰にもわかりません!)。実際に使用することができます (Web フレームワークを求めるのは多すぎますか?)

scala のような関数型言語のテスト可能性について興味深いことを聞いたことがあります。

ソフトウェアエンジニアとして、どのような選択肢がありますか?

アイデアの続き:証明可能な実世界の言語はありますか?

あなたのことはわかりませんが、保証できないコードを書くことにうんざりしています。

上記の質問をして驚異的な回答を得た後 (ありがとうございました!) Haskellへの証明可能で実用的なアプローチの検索を絞り込むことにしました。私が Haskell を選んだのは、それが実際に有用であり (Haskell用に書かれた多くの Web フレームワークがあり、これは良いベンチマークのようです) 、機能的に十分に厳密であり、証明可能であるか、少なくとも不変条件のテストが可能であると考えたからです。

これが私が欲しいものです（そして見つけることができませんでした）

psudocode で記述された Haskell 関数 add を参照できるフレームワークが必要です。

- そして、特定の不変量がすべての実行状態を保持しているかどうかを確認します。正式な証明が欲しいのですが、モデルチェッカーのようなもので解決します。
この例では、値aとbを指定すると、戻り値は常に合計a+bになります。

これは簡単な例ですが、このようなフレームワークが存在することは不可能ではないと思います。テストできる関数の複雑さには確かに上限があります (関数への 10 個の文字列入力は確かに長い時間がかかります!) が、これは関数のより慎重な設計を促進し、他の形式を使用する場合と違いはありません。メソッド。Z または B を使用することを想像してみてください。変数/セットを定義するときは、変数に可能な限り小さい範囲を指定するようにしてください。INT が 100 を超えることがない場合は、そのように初期化してください。このような手法と適切な問題分解により、Haskell のような純粋関数型言語の十分なチェックが可能になるはずです。

私は正式なメソッドや Haskell の経験はまだありません。私のアイデアが正しいものなのか、それとも Haskell は適していないと思うのか教えてください 別の言語を提案する場合は、「has-a-web-framework」テストに合格することを確認し、元の質問を読んでください:-)

KDE などの大規模で実世界のほとんどが C++ の分散システムのモデル チェックを処理できるツールはありますか?

(KDE は IPC を使用するという意味で分散システムですが、通常はすべてのプロセスが同じマシン上にあります。はい、ちなみに、これは「分散システム」の有効な使用法です - ウィキペディアを確認してください。)

このツールは、プロセス内イベントとプロセス間メッセージを処理できる必要があります。

(ツールが C++ をサポートしているが、moc などの KDE が使用する他のものをサポートしていない場合、何かをハックして回避できると仮定しましょう。)

実際のモデル チェッカーの代わりに、あまり一般的でないもの (特定のクラスのバグを見つけることに特化した静的アナライザーなど) またはより一般的な静的解析の代替手段を喜んで受け入れます。しかし、私が興味を持っているのは、KDE ​​の規模と複雑さのプロジェクトを実際に処理できるツールだけです。

API を記述する言語に依存しない正式な言語はありますか? 多くのアーキテクチャで使用されるユーティリティ ライブラリを定義したいと考えており、すべての API 関数が実装されていることをプログラムでテストし、理想的にはプラットフォーム全体で関数の単体テストを実行する方法が必要です。

たとえば、.Net アセンブリを C# で、Windows DLL を C++ で、MacOS ライブラリを Objective-C で、Linux 共有ライブラリを C++ で記述したいと考えています。

コード コントラクトで装飾した簡単なグラフ操作メソッドを次に示します。

ensure クレームは証明されませんが、理由がわかりません! Remove() を呼び出した後、エッジがエッジ リストにないか、結果が false であると主張していると思います。結果が true の場合、グラフの状態については何も主張しません。静的チェッカーはそれを気に入らず、Pex にその方法を教えてもらっていません (ただし、おそらく使い方がわからないだけです)。

この例ではロックは無関係だと思いますが、念のためそのままにしておきます。また、OnRemoveEdge のデリゲートには何の保証もありませんが、ここでは、Graph コードに再入可能ではないと暗黙的に仮定します。その上、仮定はその後です。

更新: コードを変更して、イベント ハンドラー OnRemoveEdge() (ただし、デリゲート OnBeforeRemoveEdge は除く) をロックから外しました。しかし、これは、スレッドに関連するコントラクトの前提に対して何をするのでしょうか? コード コントラクトはシングル スレッド モデルを想定していますか? うーん。

一部のロボットコントローラーが、一連の述語で定義する障害状態に到達しないことを証明することに興味があります。それを実現するためのオープンソースソフトウェアツールがあることを私は知っています。たとえば、BLAST（Berkeley Lazy Abstraction Software Verification Tool）について聞いたことがありますが、他に、より簡単に使用できる、および/または特定のアプリケーションを対象としたものを知っていますか？

プロジェクトの1つでBLASTまたは別のそのようなツールを使用したことがありますか。また、そのようなツールを展開するために必要な労力よりもメリットが大きいと思いますか。

私はFrama-Cの初心者ユーザーであり、ポインターに対するアサーションに関していくつか質問があります。

以下のCフラグメントについて考えてみます。

• 2つの関連するデータ構造DataとHandle、stHandleにはDataへのポインターがあります。
• いくつかの架空の操作が完了したかどうかを示すデータの「状態」フィールド
• 3つの関数：init（）、start_operation（）、wait（）;
• 上記を使用し、6つのアサーションを含むmain（）関数（A1-A6）

さて、なぜA5とA6はWPベリファイア（ "frama-c -wp file.c"）でアサートできないのですか？start_operation（）の最後の "ensures"句のために保持されるべきではありませんか？

私は何が間違っているのですか？

一番、

エドゥアルド

SMT ソルバーは、SAT と同様に充足可能性を考慮して開発されています。私たちが知っているように、SATは充足可能性のためでもあり、SATの変形が提案されています。それらの 1 つが max-SAT です。そこで、max-SMT ソルバーが存在するかどうか、存在する場合はどのように機能するのかをお尋ねしたいと思います。