問題タブ [model-checking]

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

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

私はもう試した

しかし、TLCは私に構文エラーを与えます：

エラー：TLCは、1行目の構成ファイルでエラーを検出しました。=または<-を予期していましたが、検出されませんでした。

Sequencesまた、モジュールを構成ファイルに含めようとしましたが、役に立ちませんでした。

だから...シーケンスを割り当てるために私は何をしなければなりませんか？

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

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

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

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

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

誰かがこのツールSPINを使ったモデル検査、さらにモデル検査の情報（並行プログラム）に触れたことはありますか

クロック変数の現在の値を取得して整数変数に格納する方法を教えてください。k=t (k は整数、t はクロック) を試しましたが、「互換性のない型エラー」がスローされます。k=(int)t も試しましたが、「予期しない T_INT」構文エラーがスローされます。

時計の現在の値を取得して変数に格納するために、UPPAAL の時計で使用できる型キャストはありますか?

Spin Model Checker を使用して、2 つのオブジェクト (A と B) 間のゲームをモデルチェックしようとしています。オブジェクトはボード上を移動し、各位置はその (x,y) 座標によって定義されます。2 つのオブジェクトは衝突しないはずです。init、A Model、B Model の 3 つのプロセスがあります。私は ltl プロパティをチェックするモデルです: (2 つのオブジェクトが同じ場所を占有するかどうかをチェックする liveness プロパティ)

私が得るエラートレイルは次のとおりです: init -> A Model -> B Model -> init

ただし、表示されているデータに基づいてエラー トレイル (反例) を取得する必要はありません: x_a=2、x_b=1、y_a=1、y_b=1。

また、最初の init は init プロセスのすべての行を通過しますが、2 番目の init はその最後の行までしか表示されません。

また、私の A モデルと B モデルは、以下に示すように、「do」ブロック内のガードとアクションのみで構成されています。ただし、それらはより複雑で、'->' の右側に if ブロックがあります。

アトミックブロックに何かを入れる必要はありますか? 私が質問している理由は、エラー トレイルが示している行が 'do' ブロックにも入っておらず、2 つのモデルの最初の行に過ぎないからです。

編集: LTL プロパティが間違っていました。私はそれを次のように変更しました：

しかし、私はまだまったく同じエラートレイルを取得しています。

コンセンサス アルゴリズムを実装しました (Paxos に基づく)。ランダムなテストケースをいくつか追加しましたが、問題ないようです。しかし、モデル チェックを介してテストを行いたいですか? 適切な記事が見つかりませんでした。Paxos でのモデル チェックの方法を共有してください

ありがとう

C# コード用のモデル チェック ライブラリはありますか? Eiffel のように、事前、事後条件注釈のクラス不変条件を探しています。私はSpec#をグーグルで検索しましたが、私が理解したように、それは言語拡張であり、私が期待するライブラリではありません.

ありがとう！

エッジのガードを次のように構成したいと思います。

ここで、turnはクロック変数であり、meはプロセスを表すintです。

上記の述語をガードする方法の例を教えてください。

ありがとう、ケビン

私はAlloyで足を濡らそうとしています（これも比較的新しいもので、正式なロジックでもあります）。また、ノードの完全に接続されたグラフから始めようとしています。

画像からわかるように、ノード0と1は接続されていません。私の事実はそれを完全に接続するのに十分だと思いました...しかし、おそらく私は何かを逃しました。