リアルタイム システムを検証するために、Timed Automata について詳しく知りたいです。現在、私は UPPAAL というツールに慣れようとしています。
簡単なグラフをいくつか描き、さまざまなプロパティを追加しました。モデル全体は、異なる機械ユニットがブロックを相互に受け渡す生産セル システムを表すと想定されています。
ブロック ( BlockCycle )、2 つの機械ユニット ( Feeder、FeederBelt )、およびブロックの到着を感知する 2 つのセンサーをモデル化しました。
私のシステムは理にかなっていると思っていましたが、行き詰まりました。
この遷移のターゲット状態は、不変条件に違反しています。モデルがこのように動作することを意図している限り、これは問題ではありません。
（いいえ、しませんでした。;P）
しかし、デッドロックの理由を見つけることができないようです。このツールはBlockCycleモデルを示していますが、そこで不変条件を指定していません。実際、すべての移行要件が満たされているため、移行 ( Pos7 からPos8へ)は確実に実行する必要があります。
以下に、システムがどのように進化し、最終的にスタックするかを示します (エラー メッセージが表示されます)。
ラベル:
- 緑 : プロパティ チェック (例: FB_RunningはFB_Running == trueを意味します)
- 濃い青: プロパティの更新/割り当て
- 濃い赤: ロケーション (例: Pos7またはPos8 )
問題のそれぞれの遷移を含む BlockCycleモデル:
私の質問: 実行できるトランザクションがまだあるのに、システムがデッドロックするのはなぜですか。
Edit1: Sensor7 の位置Active ( BlockAtPos[7]と呼ばれる) の不変プロパティを削除すると、デッドロックが解決されます。したがって、デッドロックする前の最後の遷移でSensor7とBlockCycleの間に同期がないため、矛盾が発生すると思います ( BlockAtPos[7]が false になる一方で、センサーはInActive遷移を行う機会がまだありません)。不変条件に違反しています。
注: 私の UPPAAL コード/ファイルはpcs.xmlにあります。