問題タブ [model-checking]

Daniel Jackson の優れた本 ( Software Abstractions)の例、具体的にはリーダーを選出するために彼がトークンリングをセットアップしている例に従っています。

この例 (リング選挙) を拡張して、トークンが 1 つに限定されるのではなく、指定された時間内にすべてのメンバーに渡されるようにしようとしています (各メンバーは複数回ではなく 1 回だけ選出されます)。ただし (主に合金の経験が浅いため)、最善の方法を見つけるのに問題があります。最初は、いくつかの演算子 (- を + に変更) をいじれると思っていましたが、うまくいきませんでした。

以下は、例のコードです。私は質問でいくつかの領域をマークアップしました...すべての助けに感謝します。アロイ4.2を使用しています。

この質問からのフォローアップ...

完全に接続されたグラフがあります。これは素晴らしいことです。時間の概念も追加しました。現在、グラフの周りにデータを渡すという概念に苦労しています。

システムに挿入されたデータのコピーが各ノードにあることを確認するタスクを持つシステムをモデル化しています。これを行う方法については頭の中に手順がありますが、それを合金の用語に翻訳するのに苦労しています。

典型的なアルゴリズムは次のようになります。

簡単にするために、各ノードには一意のデータがあり、そのデータを他のすべてのノードに提供する必要があるとしましょう。これは完全に接続されているため、比較的簡単なはずです (合金/形式ロジックへの変換は、私にとっては少し難しいです)。

これは私が現在いる場所です：

私の run 述語から、すべてのメッセージを 20 時間ステップ以内に送信したいことがわかります。そのため、各 DataMirror には、その時間までに 5 つの一意のメッセージで構成されるデータ セットが必要です。

私がやりたいことは、各 DataMirror に 2 つのプロパティを持たせることだと確信しています。

• 送信する一意のメッセージ (この時点では単純な変数にすることができます)
• 受信したメッセージのセット (元のメッセージを含む)

すべての DataMirror が同じメッセージ セットを持っている場合、システムは満足します。

たとえば、次の場合:

次に、システムは次の場合に満たされます。

正式なロジックのパワーユーザーをうんざりさせてしまったことを前もってお詫びします...私は火の試練でこれを学ぼうとしています:)。

Alloy で偶発的な故障をモデル化することは可能ですか?

たとえば、現在、さまざまな時間ステップでデータを隣接グラフに渡す接続グラフがあります。私がやろうとしているのは、モデルがリンクをランダムに強制終了できるようにする方法を見つけ出し、そうすることで、その目標を達成することです (すべてのノードのデータ状態がオンに設定されていることを確認する)。

私がモデリングしようとしているソフトウェアは、不確実性を扱っています。基本的に、ノード間のリンクが失敗する可能性があり、ソフトウェアは別のパスに沿って再ルーティングします。私が Alloy でやりたいと思っていることは、リンクが特定のタイムステップで (できればランダムに) '死ぬ' ための機能を持たせることです。最上位の事実として、私はグラフを完全に接続する機能を持っているため、リンクが停止した場合、別のリンクがたるみを拾う可能性があります (simple_change が Datum の状態を On に切り替えるため)。接続されているすべてのネイバー)。

編集：

それで、提案されたとおりに実行したところ、次のエラーが発生しました。
隣人とノードがまだ設定されていると思っていたので、混乱していますか?

これが私の更新されたコードです：

C言語で書かれたターゲットプログラムのループをソースコードレベルで自動巻き戻ししたい(参考までにlinuxとgccコンパイラを使っています)。詳細な説明については、次の簡単なソース コードを見てみましょう。

上記のソースコードを次のように変換したいと思います。

CBMCがソフトウェア モデル チェックのためにループを自動的に巻き戻すことは知っていますが、ループを巻き戻すために CBMC がソース コードをソース コードに変換するかどうかはわかりません。すべてのループが巻き戻されたプログラム ソース コードを取得する必要があります。

そのためのツールや解決策を見つけようとしましたが、見つかりませんでした。提案やコメントをいただければ幸いです。ありがとう！

混乱させてすみません。私の最終目標である「ソースコードレベルでのループの巻き戻し」の詳細を説明します。ループの巻き戻しの最終的な目標は、ループの巻き戻しから生成されたステートメントを実行するテスト ケースの数を測定することです。次の例を参照してください。

上記のソースコードを変換すると、次のソースコードが得られます

そして、上記の変換されたソース コードから、「ループの巻き戻し」から生じる各ステートメントを実行するテスト ケースの数を測定します。たとえば、元のソース コードの 4 行目と 5 行目から変換された 3、4 行目、7、8 行目、または 11、12 行目を実行するテスト ケースの数は、1 行を実行するテスト ケースの数とは異なります。元のソース コードの #4,5。

参考までに、ループを巻き戻さずに最終目標を達成できる方法があれば、その方法も良いです! ありがとう！

以下は、私が最近携帯電話のテキストメッセージ用に完成させたまあまあの合金仕様です。それは単なる基本的なテキストメッセージの要件であり、それは慣習であるため、私は守るべき厳格な要件はありません。ただし、Name-Mobileペアのペアを1つしか取得できないなど、いくつかの厄介な問題があります。2つのメッセージセットが一貫して1つの名前を指しているのはなぜですか？質問を除いて、事実と述語は非常に単純です。合金自体を学ぶためのフィードバックが必要ですので、十分に批判してください。

以下のことをしているときに私が心に留めていたこと;

1つのメッセージボックスに0個以上のメッセージセットがあります。セットは1人のみに属し、セットは無料ではありません。各セットには、メッセージ行、開始キーと終了キー、行、およびカーソル位置で構成される1つ以上のメッセージがあります。複数のメッセージが同じ人に属することはできますが、同時に2人に属することはできません。各行には1つ以上のキーがあり、開始キーと終了キーがあります。また、行には新しい行がある場合とない場合があります。各キーには、次のキーがある場合とない場合があります。キーはタッチパッドを介して押されます。すべての名前には携帯電話番号があり、ContactListに記録されます。2人の名前が同じ携帯電話を持つことはできませんが、人は複数の電話番号を持つことができます。

ありがとう。

不変条件に違反した場合に、アルゴリズムによって返される反例の長さが最小になるように、Kripke 構造に対する不変条件をチェックするための (疑似コード) アルゴリズムは何ですか?

ダイクストラが「シーケンシャルプロセスの協調」というタイトルの論文で書いたALGOL60コードを再現しようとしています。このコードは、ミューテックス問題を解決する最初の試みです。構文は次のとおりです。

だから私はPromelaで上記のコードを再現しようとしました、そしてここに私のコードがあります：

私がやろうとしているのは、ラベルL1が無限に実行されているため、公平性プロパティが保持されないことを確認することです。

ここでの問題は、neverclaimブロックがエラーを生成していないことです。取得した出力は、単に私のステートメントに到達しなかったことを示しています。

これがiSpinからの実際の出力です

ブロックのスピンに関するすべてのドキュメントを読みましたnever{..}が、答えが見つかりませんでした（ここにリンクがあります）。また、ltl{..}ブロックを使用してみました（リンク）が、明示的には構文エラーが発生しました。ドキュメントに、initおよびの外部にある可能性があると記載されていますがproctypes、誰かがこのコードを修正するのを手伝ってもらえますか？

ありがとうございました

次のLTLプロパティの単純なPromelaモデルをモデルチェックしようとしています:

そして、エラーが発生しました。エラートレイルのガイド付きシミュレーションでは、次の出力が得られます。

ここで、「M[0] until M[1]」がどこで違反されているのかわかりません。M[0] は init プロセスで 1 に設定され、M[1] が 1 になるまでそのままです。トレースが非常に早く終了するか、「stronguntil」のセマンティクスを完全に誤解している可能性があります。私はこれが事実であると確信しています...しかし、私は何が間違っていますか? Promela ファイル内の LTL の指定は大丈夫ですか?

問題のモデルは次のとおりです (単純なペトリネット)。

LTL 数式のサイズ |p| は一般的に、複雑さに関して何を意味しますか? 原子命題の数、深さ、または何か？

前もって感謝します！！