model-checking

1熱

1答えて

モデルチェッカーを使用して特定のトレースを確認してください

私はオープン相互作用プロトコルのルールを定義するためにLTLを使用しています。私は、特定の対話が仕様に従っているかどうか、または何らかのルールが壊れていないかどうかを確認したい。私の直接のアプローチはNuSMVを使うことでしたが、問題は私がチェックしたい相互作用のモデルではなく、ただ一つの特定の有限のトレース（すべての状態のすべての変数の値）です。 これをNuSMVで指定できる方法はありますか？

logic formal-verification model-checking nusmv 2016-09-19

---

2熱

2答えて

BDDの変数をCUDDパッケージで置き換えるにはどうすればよいですか？

DdManagerには、x, y, x', y'という変数があり、BDDはxとyで作成されています。 は、今私は、すなわち、x'とy'によって構築された、同一のBDDを取得し、y'にx'からx、yを変更したいです。 CUDDパッケージを使用してこれを取得するにはどうすればよいですか？私はモデル検査アルゴリズムを実装したいときにこの問題に遭遇しました。私はこの操作を実装する方法を知りたいか、シンボリ

model-checking binary-decision-diagram cudd 2017-02-24

---

2熱

1答えて

状態空間がシステムの動作の正式な仕様であると言うことができますか？

システムとその完全な状態空間が与えられれば、その状態空間はそのシステムの動作の正式な仕様であると言うことができますか？

verification formal-verification model-checking formal-methods 2016-06-29

---

0熱

1答えて

システムにデッドロックが含まれています - どのようにそれを見つけるのですか？ （UPPAAL）

私はUPPAALでモデルを設定しました。私はデベロッパーがデッドロックをチェックするために検証を使用しました。答えは：プロパティが満たされていない。したがって、デッドロックが存在します。 UPPAALでは、特定の状況のすべての変数の状態や現在の値など、デッドロックに関する詳細な情報を報告する方法はありますか？

deadlock model-checking uppaal 2016-11-27

---

2熱

2答えて

シンボリック実行とモデルチェック

シンボリック実行と（モデル変換などの）モデル検査の違いは何ですか？私はそれらの違いを理解していない。彼らは同じですか？！

validation verification model-checking model-driven 2016-08-23

---

-1熱

1答えて

FOLモデルの一貫性チェック

私はFirst Orderロジックでモデルを開発しています。私はそれが一貫していることを証明したいと思います。出来ますか？これを行うために私が使用できる無料のツールはありますか？ これはGodel定理のために不可能ですか？ よろしくお願いいたします。

logic theorem-proving model-checking theorem 2017-03-17

---

1熱

1答えて

スピンで複数の（またはすべての）違反トレースを求める

スピンを使用してプロパティに対して複数の（またはすべての）違反トレースを取得することは可能ですか？ 例として、私は以下のPromelaモデルモデルを作成： byte mutex = 0; active proctype A() { A1: mutex==0; /* Is free? */ A2: mutex++; /* Get mutex */ A3: /* A's critical s

model-checking spin promela 2016-08-30

---

1熱

1答えて

システムモデルをモデル検査用の遷移システムに変換する

現在、システムプロトタイプを移行システムモデルに変換しようとしています。私はいくつかのLTLプロパティを持っており、モデル検査ツールNuSMVを使ってそれらのプロパティを検証したいと思います。私は、原子の性質や他の数学的な側面を定義してモデリングを始める方法に関する情報だけです。しかし、私はあなたが提供モデルはあなたに合わせて少し単純すぎることだと思う遷移システムのNuSMVで非常に単純なエンコー

fsm model-checking nusmv transition-systems 2016-07-13

---

0熱

1答えて

擬似コードをNuSMVコードに変更するにはどうすればよいですか？

私の教授は、数学の学生にNuSMVに変更するコードを与えることにしました。私は助けを求める他の場所を見つけることができず、6ページだけのような教科書を読んでいます。 Module mainはNuSMVコードの例であり、彼は擬似コードを書くためにそのフォーマット例を使用すると言いました。 whileループの記述方法と実際の設定方法がわかりません。 flag1は状態であり、また別の状態になるでしょうか

model logic model-checking nusmv 2016-05-27

---

0熱

1答えて

NuSMVでグローバル定数を定義するにはどうすればよいですか？

私はCで #define n 5 に類似した方法で、NuSMVでグローバル定数を宣言するのか分かりません。 NuSMVでどうすればいいですか？

formal-verification model-checking nusmv 2017-03-28

---